xpexr2

Description: If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006)

		Ref	Expression
	Assertion	xpexr2	$⊢ (A \times B \in C \land A \times B \neq \emptyset) \to (A \in V \land B \in V)$

Step	Hyp	Ref	Expression
1		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
2		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
3	2	adantl	$⊢ (A \times B \in C \land B \neq \emptyset) \to dom (A \times B) = A$
4		dmexg	$⊢ A \times B \in C \to dom (A \times B) \in V$
5	4	adantr	$⊢ (A \times B \in C \land B \neq \emptyset) \to dom (A \times B) \in V$
6	3 5	eqeltrrd	$⊢ (A \times B \in C \land B \neq \emptyset) \to A \in V$
7		rnxp	$⊢ A \neq \emptyset \to ran (A \times B) = B$
8	7	adantl	$⊢ (A \times B \in C \land A \neq \emptyset) \to ran (A \times B) = B$
9		rnexg	$⊢ A \times B \in C \to ran (A \times B) \in V$
10	9	adantr	$⊢ (A \times B \in C \land A \neq \emptyset) \to ran (A \times B) \in V$
11	8 10	eqeltrrd	$⊢ (A \times B \in C \land A \neq \emptyset) \to B \in V$
12	6 11	anim12dan	$⊢ (A \times B \in C \land (B \neq \emptyset \land A \neq \emptyset)) \to (A \in V \land B \in V)$
13	12	ancom2s	$⊢ (A \times B \in C \land (A \neq \emptyset \land B \neq \emptyset)) \to (A \in V \land B \in V)$
14	1 13	sylan2br	$⊢ (A \times B \in C \land A \times B \neq \emptyset) \to (A \in V \land B \in V)$

Metamath Proof Explorer