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\leftrightarrow 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\leftrightarrow {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\leftrightarrow A^{-1}\subseteq B^{-1}\right)$$