Metamath Proof Explorer

Theorem xpexg

Description: The Cartesian product of two sets is a set. Proposition 6.2 of TakeutiZaring p. 23. See also xpexgALT . (Contributed by NM, 14-Aug-1994)

		Ref	Expression
	Assertion	xpexg	$⊢ (A \in V \land B \in W) \to A \times B \in V$

Proof

Step	Hyp	Ref	Expression
1		xpsspw	$⊢ A \times B \subseteq 𝒫 𝒫 (A \cup B)$
2		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
3		pwexg	$⊢ A \cup B \in V \to 𝒫 (A \cup B) \in V$
4		pwexg	$⊢ 𝒫 (A \cup B) \in V \to 𝒫 𝒫 (A \cup B) \in V$
5	2 3 4	3syl	$⊢ (A \in V \land B \in W) \to 𝒫 𝒫 (A \cup B) \in V$
6		ssexg	$⊢ (A \times B \subseteq 𝒫 𝒫 (A \cup B) \land 𝒫 𝒫 (A \cup B) \in V) \to A \times B \in V$
7	1 5 6	sylancr	$⊢ (A \in V \land B \in W) \to A \times B \in V$