Theorem unixpid

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

	Ref	Expression
Assertion	unixpid	|- U. U. ( A X. A ) = A

Proof

Step	Hyp	Ref	Expression
1		xpeq1	|- ( A = (/) -> ( A X. A ) = ( (/) X. A ) )
2		0xp	|- ( (/) X. A ) = (/)
3	1 2	eqtrdi	|- ( A = (/) -> ( A X. A ) = (/) )
4		unieq	|- ( ( A X. A ) = (/) -> U. ( A X. A ) = U. (/) )
5	4	unieqd	|- ( ( A X. A ) = (/) -> U. U. ( A X. A ) = U. U. (/) )
6		uni0	|- U. (/) = (/)
7	6	unieqi	|- U. U. (/) = U. (/)
8	7 6	eqtri	|- U. U. (/) = (/)
9		eqtr	|- ( ( U. U. ( A X. A ) = U. U. (/) /\ U. U. (/) = (/) ) -> U. U. ( A X. A ) = (/) )
10		eqtr	|- ( ( U. U. ( A X. A ) = (/) /\ (/) = A ) -> U. U. ( A X. A ) = A )
11	10	expcom	|- ( (/) = A -> ( U. U. ( A X. A ) = (/) -> U. U. ( A X. A ) = A ) )
12	11	eqcoms	|- ( A = (/) -> ( U. U. ( A X. A ) = (/) -> U. U. ( A X. A ) = A ) )
13	9 12	syl5com	|- ( ( U. U. ( A X. A ) = U. U. (/) /\ U. U. (/) = (/) ) -> ( A = (/) -> U. U. ( A X. A ) = A ) )
14	5 8 13	sylancl	|- ( ( A X. A ) = (/) -> ( A = (/) -> U. U. ( A X. A ) = A ) )
15	3 14	mpcom	|- ( A = (/) -> U. U. ( A X. A ) = A )
16		df-ne	|- ( A =/= (/) <-> -. A = (/) )
17		xpnz	|- ( ( A =/= (/) /\ A =/= (/) ) <-> ( A X. A ) =/= (/) )
18		unixp	|- ( ( A X. A ) =/= (/) -> U. U. ( A X. A ) = ( A u. A ) )
19		unidm	|- ( A u. A ) = A
20	18 19	eqtrdi	|- ( ( A X. A ) =/= (/) -> U. U. ( A X. A ) = A )
21	17 20	sylbi	|- ( ( A =/= (/) /\ A =/= (/) ) -> U. U. ( A X. A ) = A )
22	16 16 21	sylancbr	|- ( -. A = (/) -> U. U. ( A X. A ) = A )
23	15 22	pm2.61i	|- U. U. ( A X. A ) = A