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 ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )