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