# Metamath Proof Explorer

## Theorem cnvssb

Description: Subclass theorem for converse. (Contributed by RP, 22-Oct-2020)

Ref Expression
Assertion cnvssb ${⊢}\mathrm{Rel}{A}\to \left({A}\subseteq {B}↔{{A}}^{-1}\subseteq {{B}}^{-1}\right)$

### Proof

Step Hyp Ref Expression
1 cnvss ${⊢}{A}\subseteq {B}\to {{A}}^{-1}\subseteq {{B}}^{-1}$
2 cnvss ${⊢}{{A}}^{-1}\subseteq {{B}}^{-1}\to {{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}$
3 dfrel2 ${⊢}\mathrm{Rel}{A}↔{{{A}}^{-1}}^{-1}={A}$
4 3 biimpi ${⊢}\mathrm{Rel}{A}\to {{{A}}^{-1}}^{-1}={A}$
5 4 eqcomd ${⊢}\mathrm{Rel}{A}\to {A}={{{A}}^{-1}}^{-1}$
6 5 adantr ${⊢}\left(\mathrm{Rel}{A}\wedge {{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\right)\to {A}={{{A}}^{-1}}^{-1}$
7 id ${⊢}{{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\to {{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}$
8 cnvcnvss ${⊢}{{{B}}^{-1}}^{-1}\subseteq {B}$
9 7 8 sstrdi ${⊢}{{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\to {{{A}}^{-1}}^{-1}\subseteq {B}$
10 9 adantl ${⊢}\left(\mathrm{Rel}{A}\wedge {{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\right)\to {{{A}}^{-1}}^{-1}\subseteq {B}$
11 6 10 eqsstrd ${⊢}\left(\mathrm{Rel}{A}\wedge {{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\right)\to {A}\subseteq {B}$
12 11 ex ${⊢}\mathrm{Rel}{A}\to \left({{{A}}^{-1}}^{-1}\subseteq {{{B}}^{-1}}^{-1}\to {A}\subseteq {B}\right)$
13 2 12 syl5 ${⊢}\mathrm{Rel}{A}\to \left({{A}}^{-1}\subseteq {{B}}^{-1}\to {A}\subseteq {B}\right)$
14 1 13 impbid2 ${⊢}\mathrm{Rel}{A}\to \left({A}\subseteq {B}↔{{A}}^{-1}\subseteq {{B}}^{-1}\right)$