xpexr

Description: If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006)

		Ref	Expression
	Assertion	xpexr	$⊢ A \times B \in C \to (A \in V \lor B \in V)$

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		eleq1	$⊢ A = \emptyset \to (A \in V \leftrightarrow \emptyset \in V)$
3	1 2	mpbiri	$⊢ A = \emptyset \to A \in V$
4	3	pm2.24d	$⊢ A = \emptyset \to (\neg A \in V \to B \in V)$
5	4	a1d	$⊢ A = \emptyset \to (A \times B \in C \to (\neg A \in V \to B \in V))$
6		rnexg	$⊢ A \times B \in C \to ran (A \times B) \in V$
7		rnxp	$⊢ A \neq \emptyset \to ran (A \times B) = B$
8	7	eleq1d	$⊢ A \neq \emptyset \to (ran (A \times B) \in V \leftrightarrow B \in V)$
9	6 8	syl5ib	$⊢ A \neq \emptyset \to (A \times B \in C \to B \in V)$
10	9	a1dd	$⊢ A \neq \emptyset \to (A \times B \in C \to (\neg A \in V \to B \in V))$
11	5 10	pm2.61ine	$⊢ A \times B \in C \to (\neg A \in V \to B \in V)$
12	11	orrd	$⊢ A \times B \in C \to (A \in V \lor B \in V)$

Metamath Proof Explorer