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 
|- ( A e. V -> ( A ^m 2o ) ~~ ( A X. A ) )

Proof

Step Hyp Ref Expression
1 df2o3 
 |-  2o = { (/) , 1o }
2 df-pr 
 |-  { (/) , 1o } = ( { (/) } u. { 1o } )
3 1 2 eqtri 
 |-  2o = ( { (/) } u. { 1o } )
4 3 oveq2i 
 |-  ( A ^m 2o ) = ( A ^m ( { (/) } u. { 1o } ) )
5 snex 
 |-  { (/) } e. _V
6 5 a1i 
 |-  ( A e. V -> { (/) } e. _V )
7 snex 
 |-  { 1o } e. _V
8 7 a1i 
 |-  ( A e. V -> { 1o } e. _V )
9 id 
 |-  ( A e. V -> A e. V )
10 1n0 
 |-  1o =/= (/)
11 10 neii 
 |-  -. 1o = (/)
12 elsni 
 |-  ( 1o e. { (/) } -> 1o = (/) )
13 11 12 mto 
 |-  -. 1o e. { (/) }
14 disjsn 
 |-  ( ( { (/) } i^i { 1o } ) = (/) <-> -. 1o e. { (/) } )
15 13 14 mpbir 
 |-  ( { (/) } i^i { 1o } ) = (/)
16 15 a1i 
 |-  ( A e. V -> ( { (/) } i^i { 1o } ) = (/) )
17 mapunen 
 |-  ( ( ( { (/) } e. _V /\ { 1o } e. _V /\ A e. V ) /\ ( { (/) } i^i { 1o } ) = (/) ) -> ( A ^m ( { (/) } u. { 1o } ) ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
18 6 8 9 16 17 syl31anc 
 |-  ( A e. V -> ( A ^m ( { (/) } u. { 1o } ) ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
19 4 18 eqbrtrid 
 |-  ( A e. V -> ( A ^m 2o ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
20 0ex 
 |-  (/) e. _V
21 20 a1i 
 |-  ( A e. V -> (/) e. _V )
22 9 21 mapsnend 
 |-  ( A e. V -> ( A ^m { (/) } ) ~~ A )
23 1oex 
 |-  1o e. _V
24 23 a1i 
 |-  ( A e. V -> 1o e. _V )
25 9 24 mapsnend 
 |-  ( A e. V -> ( A ^m { 1o } ) ~~ A )
26 xpen 
 |-  ( ( ( A ^m { (/) } ) ~~ A /\ ( A ^m { 1o } ) ~~ A ) -> ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) )
27 22 25 26 syl2anc 
 |-  ( A e. V -> ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) )
28 entr 
 |-  ( ( ( A ^m 2o ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) /\ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) ) -> ( A ^m 2o ) ~~ ( A X. A ) )
29 19 27 28 syl2anc 
 |-  ( A e. V -> ( A ^m 2o ) ~~ ( A X. A ) )