Metamath Proof Explorer

Theorem coundir

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	coundir	$⊢ (A \cup B) \circ C = (A \circ C) \cup (B \circ C)$

Proof

Step	Hyp	Ref	Expression
1		unopab	$⊢ \{⟨x, z⟩ \| \exists y (x C y \land y A z)\} \cup \{⟨x, z⟩ \| \exists y (x C y \land y B z)\} = \{⟨x, z⟩ \| (\exists y (x C y \land y A z) \lor \exists y (x C y \land y B z))\}$
2		brun	$⊢ y (A \cup B) z \leftrightarrow (y A z \lor y B z)$
3	2	anbi2i	$⊢ (x C y \land y (A \cup B) z) \leftrightarrow (x C y \land (y A z \lor y B z))$
4		andi	$⊢ (x C y \land (y A z \lor y B z)) \leftrightarrow ((x C y \land y A z) \lor (x C y \land y B z))$
5	3 4	bitri	$⊢ (x C y \land y (A \cup B) z) \leftrightarrow ((x C y \land y A z) \lor (x C y \land y B z))$
6	5	exbii	$⊢ \exists y (x C y \land y (A \cup B) z) \leftrightarrow \exists y ((x C y \land y A z) \lor (x C y \land y B z))$
7		19.43	$⊢ \exists y ((x C y \land y A z) \lor (x C y \land y B z)) \leftrightarrow (\exists y (x C y \land y A z) \lor \exists y (x C y \land y B z))$
8	6 7	bitr2i	$⊢ (\exists y (x C y \land y A z) \lor \exists y (x C y \land y B z)) \leftrightarrow \exists y (x C y \land y (A \cup B) z)$
9	8	opabbii	$⊢ \{⟨x, z⟩ \| (\exists y (x C y \land y A z) \lor \exists y (x C y \land y B z))\} = \{⟨x, z⟩ \| \exists y (x C y \land y (A \cup B) z)\}$
10	1 9	eqtri	$⊢ \{⟨x, z⟩ \| \exists y (x C y \land y A z)\} \cup \{⟨x, z⟩ \| \exists y (x C y \land y B z)\} = \{⟨x, z⟩ \| \exists y (x C y \land y (A \cup B) z)\}$
11		df-co	$⊢ A \circ C = \{⟨x, z⟩ \| \exists y (x C y \land y A z)\}$
12		df-co	$⊢ B \circ C = \{⟨x, z⟩ \| \exists y (x C y \land y B z)\}$
13	11 12	uneq12i	$⊢ (A \circ C) \cup (B \circ C) = \{⟨x, z⟩ \| \exists y (x C y \land y A z)\} \cup \{⟨x, z⟩ \| \exists y (x C y \land y B z)\}$
14		df-co	$⊢ (A \cup B) \circ C = \{⟨x, z⟩ \| \exists y (x C y \land y (A \cup B) z)\}$
15	10 13 14	3eqtr4ri	$⊢ (A \cup B) \circ C = (A \circ C) \cup (B \circ C)$