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

Metamath Proof Explorer

Theorem cnvun

Description: The converse of a union is the union of converses. Theorem 16 of Suppes p. 62. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		df-cnv	$⊢ {(A \cup B)}^{-1} = \{⟨x, y⟩ \| y (A \cup B) x\}$
2		unopab	$⊢ \{⟨x, y⟩ \| y A x\} \cup \{⟨x, y⟩ \| y B x\} = \{⟨x, y⟩ \| (y A x \lor y B x)\}$
3		brun	$⊢ y (A \cup B) x \leftrightarrow (y A x \lor y B x)$
4	3	opabbii	$⊢ \{⟨x, y⟩ \| y (A \cup B) x\} = \{⟨x, y⟩ \| (y A x \lor y B x)\}$
5	2 4	eqtr4i	$⊢ \{⟨x, y⟩ \| y A x\} \cup \{⟨x, y⟩ \| y B x\} = \{⟨x, y⟩ \| y (A \cup B) x\}$
6	1 5	eqtr4i	$⊢ {(A \cup B)}^{-1} = \{⟨x, y⟩ \| y A x\} \cup \{⟨x, y⟩ \| y B x\}$
7		df-cnv	$⊢ A^{-1} = \{⟨x, y⟩ \| y A x\}$
8		df-cnv	$⊢ B^{-1} = \{⟨x, y⟩ \| y B x\}$
9	7 8	uneq12i	$⊢ A^{-1} \cup B^{-1} = \{⟨x, y⟩ \| y A x\} \cup \{⟨x, y⟩ \| y B x\}$
10	6 9	eqtr4i	$⊢ {(A \cup B)}^{-1} = A^{-1} \cup B^{-1}$