This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴