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 ⊢ A ≠ ∅ ∧ B ≠ ∅ ↔ A × B ≠ ∅

Proof

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