cnvco2

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

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

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

Metamath Proof Explorer