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

Proof

Step	Hyp	Ref	Expression
1		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
2		dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
3	2	adantl	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐵 ≠ ∅ ) → dom ( 𝐴 × 𝐵 ) = 𝐴 )
4		dmexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → dom ( 𝐴 × 𝐵 ) ∈ V )
5	4	adantr	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐵 ≠ ∅ ) → dom ( 𝐴 × 𝐵 ) ∈ V )
6	3 5	eqeltrrd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ V )
7		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
8	7	adantl	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐴 ≠ ∅ ) → ran ( 𝐴 × 𝐵 ) = 𝐵 )
9		rnexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ran ( 𝐴 × 𝐵 ) ∈ V )
10	9	adantr	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐴 ≠ ∅ ) → ran ( 𝐴 × 𝐵 ) ∈ V )
11	8 10	eqeltrrd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ V )
12	6 11	anim12dan	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ ( 𝐵 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
13	12	ancom2s	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
14	1 13	sylan2br	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝐶 ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )