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	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		n0	$$⊢B\ne \varnothing \leftrightarrow \exists yy\in B$$
3	1 2	anbi12i	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow \left(\exists xx\in A\wedge \exists yy\in B\right)$$
4		exdistrv	$$⊢\exists x\exists y\left(x\in A\wedge y\in B\right)\leftrightarrow \left(\exists xx\in A\wedge \exists yy\in B\right)$$
5	3 4	bitr4i	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow \exists x\exists y\left(x\in A\wedge y\in B\right)$$
6		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
7		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in \left(A\times B\right)\leftrightarrow ⟨x,y⟩\in \left(A\times B\right)\right)$$
8		opelxp	$$⊢⟨x,y⟩\in \left(A\times B\right)\leftrightarrow \left(x\in A\wedge y\in B\right)$$
9	7 8	syl6bb	$$⊢z=⟨x,y⟩\to \left(z\in \left(A\times B\right)\leftrightarrow \left(x\in A\wedge y\in B\right)\right)$$
10	6 9	spcev	$$⊢\left(x\in A\wedge y\in B\right)\to \exists zz\in \left(A\times B\right)$$
11		n0	$$⊢A\times B\ne \varnothing \leftrightarrow \exists zz\in \left(A\times B\right)$$
12	10 11	sylibr	$$⊢\left(x\in A\wedge y\in B\right)\to A\times B\ne \varnothing$$
13	12	exlimivv	$$⊢\exists x\exists y\left(x\in A\wedge y\in B\right)\to A\times B\ne \varnothing$$
14	5 13	sylbi	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\to A\times B\ne \varnothing$$
15		xpeq1	$$⊢A=\varnothing \to A\times B=\varnothing \times B$$
16		0xp	$$⊢\varnothing \times B=\varnothing$$
17	15 16	eqtrdi	$$⊢A=\varnothing \to A\times B=\varnothing$$
18	17	necon3i	$$⊢A\times B\ne \varnothing \to A\ne \varnothing$$
19		xpeq2	$$⊢B=\varnothing \to A\times B=A\times \varnothing$$
20		xp0	$$⊢A\times \varnothing =\varnothing$$
21	19 20	eqtrdi	$$⊢B=\varnothing \to A\times B=\varnothing$$
22	21	necon3i	$$⊢A\times B\ne \varnothing \to B\ne \varnothing$$
23	18 22	jca	$$⊢A\times B\ne \varnothing \to \left(A\ne \varnothing \wedge B\ne \varnothing \right)$$
24	14 23	impbii	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$