This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ {(A \circ B)}^{-1} = B^{-1} \circ A^{-1}$

Proof

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