Theorem cnvco2

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Assertion	cnvco2	$$⊢{\left(A\circ B^{-1}\right)}^{-1}=B\circ A^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left(A\circ B^{-1}\right)}^{-1}$$
2		relco	$$⊢\mathrm{Rel}\left(B\circ A^{-1}\right)$$
3		vex	$$⊢y\in \mathrm{V}$$
4		vex	$$⊢z\in \mathrm{V}$$
5	3 4	brcnv	$$⊢y{B}^{-1}z\leftrightarrow zBy$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6 4	brcnv	$$⊢x{A}^{-1}z\leftrightarrow zAx$$
8	7	bicomi	$$⊢zAx\leftrightarrow x{A}^{-1}z$$
9	5 8	anbi12ci	$$⊢\left(y{B}^{-1}z\wedge zAx\right)\leftrightarrow \left(x{A}^{-1}z\wedge zBy\right)$$
10	9	exbii	$$⊢\exists z\left(y{B}^{-1}z\wedge zAx\right)\leftrightarrow \exists z\left(x{A}^{-1}z\wedge zBy\right)$$
11	6 3	opelcnv	$$⊢⟨x,y⟩\in {\left(A\circ B^{-1}\right)}^{-1}\leftrightarrow ⟨y,x⟩\in \left(A\circ B^{-1}\right)$$
12	3 6	opelco	$$⊢⟨y,x⟩\in \left(A\circ B^{-1}\right)\leftrightarrow \exists z\left(y{B}^{-1}z\wedge zAx\right)$$
13	11 12	bitri	$$⊢⟨x,y⟩\in {\left(A\circ B^{-1}\right)}^{-1}\leftrightarrow \exists z\left(y{B}^{-1}z\wedge zAx\right)$$
14	6 3	opelco	$$⊢⟨x,y⟩\in \left(B\circ A^{-1}\right)\leftrightarrow \exists z\left(x{A}^{-1}z\wedge zBy\right)$$
15	10 13 14	3bitr4i	$$⊢⟨x,y⟩\in {\left(A\circ B^{-1}\right)}^{-1}\leftrightarrow ⟨x,y⟩\in \left(B\circ A^{-1}\right)$$
16	1 2 15	eqrelriiv	$$⊢{\left(A\circ B^{-1}\right)}^{-1}=B\circ A^{-1}$$