Metamath Proof Explorer


Theorem map2xp

Description: A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 17-Jul-2022)

Ref Expression
Assertion map2xp ( 𝐴𝑉 → ( 𝐴m 2o ) ≈ ( 𝐴 × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df2o3 2o = { ∅ , 1o }
2 df-pr { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
3 1 2 eqtri 2o = ( { ∅ } ∪ { 1o } )
4 3 oveq2i ( 𝐴m 2o ) = ( 𝐴m ( { ∅ } ∪ { 1o } ) )
5 snex { ∅ } ∈ V
6 5 a1i ( 𝐴𝑉 → { ∅ } ∈ V )
7 snex { 1o } ∈ V
8 7 a1i ( 𝐴𝑉 → { 1o } ∈ V )
9 id ( 𝐴𝑉𝐴𝑉 )
10 1n0 1o ≠ ∅
11 10 neii ¬ 1o = ∅
12 elsni ( 1o ∈ { ∅ } → 1o = ∅ )
13 11 12 mto ¬ 1o ∈ { ∅ }
14 disjsn ( ( { ∅ } ∩ { 1o } ) = ∅ ↔ ¬ 1o ∈ { ∅ } )
15 13 14 mpbir ( { ∅ } ∩ { 1o } ) = ∅
16 15 a1i ( 𝐴𝑉 → ( { ∅ } ∩ { 1o } ) = ∅ )
17 mapunen ( ( ( { ∅ } ∈ V ∧ { 1o } ∈ V ∧ 𝐴𝑉 ) ∧ ( { ∅ } ∩ { 1o } ) = ∅ ) → ( 𝐴m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) )
18 6 8 9 16 17 syl31anc ( 𝐴𝑉 → ( 𝐴m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) )
19 4 18 eqbrtrid ( 𝐴𝑉 → ( 𝐴m 2o ) ≈ ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) )
20 0ex ∅ ∈ V
21 20 a1i ( 𝐴𝑉 → ∅ ∈ V )
22 9 21 mapsnend ( 𝐴𝑉 → ( 𝐴m { ∅ } ) ≈ 𝐴 )
23 1oex 1o ∈ V
24 23 a1i ( 𝐴𝑉 → 1o ∈ V )
25 9 24 mapsnend ( 𝐴𝑉 → ( 𝐴m { 1o } ) ≈ 𝐴 )
26 xpen ( ( ( 𝐴m { ∅ } ) ≈ 𝐴 ∧ ( 𝐴m { 1o } ) ≈ 𝐴 ) → ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) )
27 22 25 26 syl2anc ( 𝐴𝑉 → ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) )
28 entr ( ( ( 𝐴m 2o ) ≈ ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) ∧ ( ( 𝐴m { ∅ } ) × ( 𝐴m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) ) → ( 𝐴m 2o ) ≈ ( 𝐴 × 𝐴 ) )
29 19 27 28 syl2anc ( 𝐴𝑉 → ( 𝐴m 2o ) ≈ ( 𝐴 × 𝐴 ) )