Theorem 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\ne \varnothing \to \bigcup \bigcup \left(A\times B\right)=A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(A\times B\right)$$
2		relfld	$$⊢\mathrm{Rel}\left(A\times B\right)\to \bigcup \bigcup \left(A\times B\right)=\mathrm{dom}\left(A\times B\right)\cup \mathrm{ran}\left(A\times B\right)$$
3	1 2	ax-mp	$$⊢\bigcup \bigcup \left(A\times B\right)=\mathrm{dom}\left(A\times B\right)\cup \mathrm{ran}\left(A\times B\right)$$
4		xpeq2	$$⊢B=\varnothing \to A\times B=A\times \varnothing$$
5		xp0	$$⊢A\times \varnothing =\varnothing$$
6	4 5	eqtrdi	$$⊢B=\varnothing \to A\times B=\varnothing$$
7	6	necon3i	$$⊢A\times B\ne \varnothing \to B\ne \varnothing$$
8		xpeq1	$$⊢A=\varnothing \to A\times B=\varnothing \times B$$
9		0xp	$$⊢\varnothing \times B=\varnothing$$
10	8 9	eqtrdi	$$⊢A=\varnothing \to A\times B=\varnothing$$
11	10	necon3i	$$⊢A\times B\ne \varnothing \to A\ne \varnothing$$
12		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
13		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$
14		uneq12	$$⊢\left(\mathrm{dom}\left(A\times B\right)=A\wedge \mathrm{ran}\left(A\times B\right)=B\right)\to \mathrm{dom}\left(A\times B\right)\cup \mathrm{ran}\left(A\times B\right)=A\cup B$$
15	12 13 14	syl2an	$$⊢\left(B\ne \varnothing \wedge A\ne \varnothing \right)\to \mathrm{dom}\left(A\times B\right)\cup \mathrm{ran}\left(A\times B\right)=A\cup B$$
16	7 11 15	syl2anc	$$⊢A\times B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)\cup \mathrm{ran}\left(A\times B\right)=A\cup B$$
17	3 16	syl5eq	$$⊢A\times B\ne \varnothing \to \bigcup \bigcup \left(A\times B\right)=A\cup B$$