Theorem unixpid

Description: Field of a Cartesian square. (Contributed by FL, 10-Oct-2009)

	Ref	Expression
Assertion	unixpid	$$⊢\bigcup \bigcup \left(A\times A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢A=\varnothing \to A\times A=\varnothing \times A$$
2		0xp	$$⊢\varnothing \times A=\varnothing$$
3	1 2	eqtrdi	$$⊢A=\varnothing \to A\times A=\varnothing$$
4		unieq	$$⊢A\times A=\varnothing \to \bigcup \left(A\times A\right)=\bigcup \varnothing$$
5	4	unieqd	$$⊢A\times A=\varnothing \to \bigcup \bigcup \left(A\times A\right)=\bigcup \bigcup \varnothing$$
6		uni0	$$⊢\bigcup \varnothing =\varnothing$$
7	6	unieqi	$$⊢\bigcup \bigcup \varnothing =\bigcup \varnothing$$
8	7 6	eqtri	$$⊢\bigcup \bigcup \varnothing =\varnothing$$
9		eqtr	$$⊢\left(\bigcup \bigcup \left(A\times A\right)=\bigcup \bigcup \varnothing \wedge \bigcup \bigcup \varnothing =\varnothing \right)\to \bigcup \bigcup \left(A\times A\right)=\varnothing$$
10		eqtr	$$⊢\left(\bigcup \bigcup \left(A\times A\right)=\varnothing \wedge \varnothing =A\right)\to \bigcup \bigcup \left(A\times A\right)=A$$
11	10	expcom	$$⊢\varnothing =A\to \left(\bigcup \bigcup \left(A\times A\right)=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A\right)$$
12	11	eqcoms	$$⊢A=\varnothing \to \left(\bigcup \bigcup \left(A\times A\right)=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A\right)$$
13	9 12	syl5com	$$⊢\left(\bigcup \bigcup \left(A\times A\right)=\bigcup \bigcup \varnothing \wedge \bigcup \bigcup \varnothing =\varnothing \right)\to \left(A=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A\right)$$
14	5 8 13	sylancl	$$⊢A\times A=\varnothing \to \left(A=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A\right)$$
15	3 14	mpcom	$$⊢A=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A$$
16		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
17		xpnz	$$⊢\left(A\ne \varnothing \wedge A\ne \varnothing \right)\leftrightarrow A\times A\ne \varnothing$$
18		unixp	$$⊢A\times A\ne \varnothing \to \bigcup \bigcup \left(A\times A\right)=A\cup A$$
19		unidm	$$⊢A\cup A=A$$
20	18 19	eqtrdi	$$⊢A\times A\ne \varnothing \to \bigcup \bigcup \left(A\times A\right)=A$$
21	17 20	sylbi	$$⊢\left(A\ne \varnothing \wedge A\ne \varnothing \right)\to \bigcup \bigcup \left(A\times A\right)=A$$
22	16 16 21	sylancbr	$$⊢\neg A=\varnothing \to \bigcup \bigcup \left(A\times A\right)=A$$
23	15 22	pm2.61i	$$⊢\bigcup \bigcup \left(A\times A\right)=A$$