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

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