xpundi

Description: Distributive law for Cartesian product over union. Theorem 103 of Suppes p. 52. (Contributed by NM, 12-Aug-2004)

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

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

Metamath Proof Explorer