This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )