Theorem unixp0

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

	Ref	Expression
Assertion	unixp0	$$⊢A\times B=\varnothing \leftrightarrow \bigcup \left(A\times B\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢A\times B=\varnothing \to \bigcup \left(A\times B\right)=\bigcup \varnothing$$
2		uni0	$$⊢\bigcup \varnothing =\varnothing$$
3	1 2	eqtrdi	$$⊢A\times B=\varnothing \to \bigcup \left(A\times B\right)=\varnothing$$
4		n0	$$⊢A\times B\ne \varnothing \leftrightarrow \exists zz\in \left(A\times B\right)$$
5		elxp3	$$⊢z\in \left(A\times B\right)\leftrightarrow \exists x\exists y\left(⟨x,y⟩=z\wedge ⟨x,y⟩\in \left(A\times B\right)\right)$$
6		elssuni	$$⊢⟨x,y⟩\in \left(A\times B\right)\to ⟨x,y⟩\subseteq \bigcup \left(A\times B\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	opnzi	$$⊢⟨x,y⟩\ne \varnothing$$
10		ssn0	$$⊢\left(⟨x,y⟩\subseteq \bigcup \left(A\times B\right)\wedge ⟨x,y⟩\ne \varnothing \right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
11	6 9 10	sylancl	$$⊢⟨x,y⟩\in \left(A\times B\right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
12	11	adantl	$$⊢\left(⟨x,y⟩=z\wedge ⟨x,y⟩\in \left(A\times B\right)\right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
13	12	exlimivv	$$⊢\exists x\exists y\left(⟨x,y⟩=z\wedge ⟨x,y⟩\in \left(A\times B\right)\right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
14	5 13	sylbi	$$⊢z\in \left(A\times B\right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
15	14	exlimiv	$$⊢\exists zz\in \left(A\times B\right)\to \bigcup \left(A\times B\right)\ne \varnothing$$
16	4 15	sylbi	$$⊢A\times B\ne \varnothing \to \bigcup \left(A\times B\right)\ne \varnothing$$
17	16	necon4i	$$⊢\bigcup \left(A\times B\right)=\varnothing \to A\times B=\varnothing$$
18	3 17	impbii	$$⊢A\times B=\varnothing \leftrightarrow \bigcup \left(A\times B\right)=\varnothing$$