Theorem cnvco

Description: Distributive law of converse over class composition. Theorem 26 of Suppes p. 64. (Contributed by NM, 19-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		exancom	$$⊢\exists z\left(xBz\wedge zAy\right)\leftrightarrow \exists z\left(zAy\wedge xBz\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	brco	$$⊢x\left(A\circ B\right)y\leftrightarrow \exists z\left(xBz\wedge zAy\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6	3 5	brcnv	$$⊢y{A}^{-1}z\leftrightarrow zAy$$
7	5 2	brcnv	$$⊢z{B}^{-1}x\leftrightarrow xBz$$
8	6 7	anbi12i	$$⊢\left(y{A}^{-1}z\wedge z{B}^{-1}x\right)\leftrightarrow \left(zAy\wedge xBz\right)$$
9	8	exbii	$$⊢\exists z\left(y{A}^{-1}z\wedge z{B}^{-1}x\right)\leftrightarrow \exists z\left(zAy\wedge xBz\right)$$
10	1 4 9	3bitr4i	$$⊢x\left(A\circ B\right)y\leftrightarrow \exists z\left(y{A}^{-1}z\wedge z{B}^{-1}x\right)$$
11	10	opabbii	$$⊢\left\{⟨y,x⟩|x\left(A\circ B\right)y\right\}=\left\{⟨y,x⟩|\exists z\left(y{A}^{-1}z\wedge z{B}^{-1}x\right)\right\}$$
12		df-cnv	$$⊢{\left(A\circ B\right)}^{-1}=\left\{⟨y,x⟩|x\left(A\circ B\right)y\right\}$$
13		df-co	$$⊢B^{-1}\circ A^{-1}=\left\{⟨y,x⟩|\exists z\left(y{A}^{-1}z\wedge z{B}^{-1}x\right)\right\}$$
14	11 12 13	3eqtr4i	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$