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