Theorem unixpid

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

	Ref	Expression
Assertion	unixpid	⊢ ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		xpeq1	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ( ∅ × 𝐴 ) )
2		0xp	⊢ ( ∅ × 𝐴 ) = ∅
3	1 2	eqtrdi	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ∅ )
4		unieq	⊢ ( ( 𝐴 × 𝐴 ) = ∅ → ∪ ( 𝐴 × 𝐴 ) = ∪ ∅ )
5	4	unieqd	⊢ ( ( 𝐴 × 𝐴 ) = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = ∪ ∪ ∅ )
6		uni0	⊢ ∪ ∅ = ∅
7	6	unieqi	⊢ ∪ ∪ ∅ = ∪ ∅
8	7 6	eqtri	⊢ ∪ ∪ ∅ = ∅
9		eqtr	⊢ ( ( ∪ ∪ ( 𝐴 × 𝐴 ) = ∪ ∪ ∅ ∧ ∪ ∪ ∅ = ∅ ) → ∪ ∪ ( 𝐴 × 𝐴 ) = ∅ )
10		eqtr	⊢ ( ( ∪ ∪ ( 𝐴 × 𝐴 ) = ∅ ∧ ∅ = 𝐴 ) → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 )
11	10	expcom	⊢ ( ∅ = 𝐴 → ( ∪ ∪ ( 𝐴 × 𝐴 ) = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 ) )
12	11	eqcoms	⊢ ( 𝐴 = ∅ → ( ∪ ∪ ( 𝐴 × 𝐴 ) = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 ) )
13	9 12	syl5com	⊢ ( ( ∪ ∪ ( 𝐴 × 𝐴 ) = ∪ ∪ ∅ ∧ ∪ ∪ ∅ = ∅ ) → ( 𝐴 = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 ) )
14	5 8 13	sylancl	⊢ ( ( 𝐴 × 𝐴 ) = ∅ → ( 𝐴 = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 ) )
15	3 14	mpcom	⊢ ( 𝐴 = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 )
16		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
17		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) ↔ ( 𝐴 × 𝐴 ) ≠ ∅ )
18		unixp	⊢ ( ( 𝐴 × 𝐴 ) ≠ ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = ( 𝐴 ∪ 𝐴 ) )
19		unidm	⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
20	18 19	eqtrdi	⊢ ( ( 𝐴 × 𝐴 ) ≠ ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 )
21	17 20	sylbi	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ ∅ ) → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 )
22	16 16 21	sylancbr	⊢ ( ¬ 𝐴 = ∅ → ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 )
23	15 22	pm2.61i	⊢ ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴