xpundir

Description: Distributive law for Cartesian product over union. Similar to Theorem 103 of Suppes p. 52. (Contributed by NM, 30-Sep-2002)

		Ref	Expression
	Assertion	xpundir	$⊢ (A \cup B) \times C = (A \times C) \cup (B \times C)$

Step	Hyp	Ref	Expression
1		df-xp	$⊢ (A \cup B) \times C = \{⟨x, y⟩ \| (x \in (A \cup B) \land y \in C)\}$
2		df-xp	$⊢ A \times C = \{⟨x, y⟩ \| (x \in A \land y \in C)\}$
3		df-xp	$⊢ B \times C = \{⟨x, y⟩ \| (x \in B \land y \in C)\}$
4	2 3	uneq12i	$⊢ (A \times C) \cup (B \times C) = \{⟨x, y⟩ \| (x \in A \land y \in C)\} \cup \{⟨x, y⟩ \| (x \in B \land y \in C)\}$
5		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
6	5	anbi1i	$⊢ (x \in (A \cup B) \land y \in C) \leftrightarrow ((x \in A \lor x \in B) \land y \in C)$
7		andir	$⊢ ((x \in A \lor x \in B) \land y \in C) \leftrightarrow ((x \in A \land y \in C) \lor (x \in B \land y \in C))$
8	6 7	bitri	$⊢ (x \in (A \cup B) \land y \in C) \leftrightarrow ((x \in A \land y \in C) \lor (x \in B \land y \in C))$
9	8	opabbii	$⊢ \{⟨x, y⟩ \| (x \in (A \cup B) \land y \in C)\} = \{⟨x, y⟩ \| ((x \in A \land y \in C) \lor (x \in B \land y \in C))\}$
10		unopab	$⊢ \{⟨x, y⟩ \| (x \in A \land y \in C)\} \cup \{⟨x, y⟩ \| (x \in B \land y \in C)\} = \{⟨x, y⟩ \| ((x \in A \land y \in C) \lor (x \in B \land y \in C))\}$
11	9 10	eqtr4i	$⊢ \{⟨x, y⟩ \| (x \in (A \cup B) \land y \in C)\} = \{⟨x, y⟩ \| (x \in A \land y \in C)\} \cup \{⟨x, y⟩ \| (x \in B \land y \in C)\}$
12	4 11	eqtr4i	$⊢ (A \times C) \cup (B \times C) = \{⟨x, y⟩ \| (x \in (A \cup B) \land y \in C)\}$
13	1 12	eqtr4i	$⊢ (A \cup B) \times C = (A \times C) \cup (B \times C)$

Metamath Proof Explorer