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

Metamath Proof Explorer

Theorem xpnz

Description: The Cartesian product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by NM, 30-Jun-2006)

Ref Expression
Assertion xpnz ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
3 1 2 anbi12i ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) )
4 exdistrv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) )
5 3 4 bitr4i ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
6 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
7 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
8 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
9 7 8 bitrdi ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
10 6 9 spcev ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 𝑧 ∈ ( 𝐴 × 𝐵 ) )
11 n0 ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐴 × 𝐵 ) )
12 10 11 sylibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
13 12 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
14 5 13 sylbi ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
15 xpeq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐵 ) = ( ∅ × 𝐵 ) )
16 0xp ⊢ ( ∅ × 𝐵 ) = ∅
17 15 16 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
18 17 necon3i ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → 𝐴 ≠ ∅ )
19 xpeq2 ⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
20 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
21 19 20 eqtrdi ⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
22 21 necon3i ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → 𝐵 ≠ ∅ )
23 18 22 jca ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
24 14 23 impbii ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )