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

Metamath Proof Explorer

Theorem unixp0

Description: A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006)

Ref Expression
Assertion unixp0 ( ( 𝐴 × 𝐵 ) = ∅ ↔ ∪ ( 𝐴 × 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 unieq ⊢ ( ( 𝐴 × 𝐵 ) = ∅ → ∪ ( 𝐴 × 𝐵 ) = ∪ ∅ )
2 uni0 ⊢ ∪ ∅ = ∅
3 1 2 eqtrdi ⊢ ( ( 𝐴 × 𝐵 ) = ∅ → ∪ ( 𝐴 × 𝐵 ) = ∅ )
4 n0 ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐴 × 𝐵 ) )
5 elxp3 ⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
6 elssuni ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ⊆ ∪ ( 𝐴 × 𝐵 ) )
7 vex ⊢ 𝑥 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 opnzi ⊢ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅
10 ssn0 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ⊆ ∪ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅ ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
11 6 9 10 sylancl ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
12 11 adantl ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
13 12 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
14 5 13 sylbi ⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
15 14 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐴 × 𝐵 ) → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
16 4 15 sylbi ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ∪ ( 𝐴 × 𝐵 ) ≠ ∅ )
17 16 necon4i ⊢ ( ∪ ( 𝐴 × 𝐵 ) = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
18 3 17 impbii ⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ∪ ( 𝐴 × 𝐵 ) = ∅ )