cnvco1

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

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

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

Metamath Proof Explorer