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 = \emptyset \leftrightarrow ⋃ (A \times B) = \emptyset$

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

Metamath Proof Explorer