Theorem 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	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ ∅ ∈ V ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
4	3	pm2.24d	⊢ ( 𝐴 = ∅ → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) )
5	4	a1d	⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) ) )
6		rnexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ran ( 𝐴 × 𝐵 ) ∈ V )
7		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
8	7	eleq1d	⊢ ( 𝐴 ≠ ∅ → ( ran ( 𝐴 × 𝐵 ) ∈ V ↔ 𝐵 ∈ V ) )
9	6 8	imbitrid	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → 𝐵 ∈ V ) )
10	9	a1dd	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) ) )
11	5 10	pm2.61ine	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) )
12	11	orrd	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) )