unixp

Description: The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006)

		Ref	Expression
	Assertion	unixp	$⊢ A \times B \neq \emptyset \to ⋃ ⋃ (A \times B) = A \cup B$

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (A \times B)$
2		relfld	$⊢ Rel (A \times B) \to ⋃ ⋃ (A \times B) = dom (A \times B) \cup ran (A \times B)$
3	1 2	ax-mp	$⊢ ⋃ ⋃ (A \times B) = dom (A \times B) \cup ran (A \times B)$
4		xpeq2	$⊢ B = \emptyset \to A \times B = A \times \emptyset$
5		xp0	$⊢ A \times \emptyset = \emptyset$
6	4 5	eqtrdi	$⊢ B = \emptyset \to A \times B = \emptyset$
7	6	necon3i	$⊢ A \times B \neq \emptyset \to B \neq \emptyset$
8		xpeq1	$⊢ A = \emptyset \to A \times B = \emptyset \times B$
9		0xp	$⊢ \emptyset \times B = \emptyset$
10	8 9	eqtrdi	$⊢ A = \emptyset \to A \times B = \emptyset$
11	10	necon3i	$⊢ A \times B \neq \emptyset \to A \neq \emptyset$
12		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
13		rnxp	$⊢ A \neq \emptyset \to ran (A \times B) = B$
14		uneq12	$⊢ (dom (A \times B) = A \land ran (A \times B) = B) \to dom (A \times B) \cup ran (A \times B) = A \cup B$
15	12 13 14	syl2an	$⊢ (B \neq \emptyset \land A \neq \emptyset) \to dom (A \times B) \cup ran (A \times B) = A \cup B$
16	7 11 15	syl2anc	$⊢ A \times B \neq \emptyset \to dom (A \times B) \cup ran (A \times B) = A \cup B$
17	3 16	eqtrid	$⊢ A \times B \neq \emptyset \to ⋃ ⋃ (A \times B) = A \cup B$

Metamath Proof Explorer