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	⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ∪ ( 𝐴 × 𝐵 ) = ∅ )