Metamath Proof Explorer


Theorem map1

Description: Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of Mendelson p. 255. (Contributed by NM, 17-Dec-2003) (Proof shortened by AV, 17-Jul-2022)

Ref Expression
Assertion map1
|- ( A e. V -> ( 1o ^m A ) ~~ 1o )

Proof

Step Hyp Ref Expression
1 df1o2
 |-  1o = { (/) }
2 1 oveq1i
 |-  ( 1o ^m A ) = ( { (/) } ^m A )
3 0ex
 |-  (/) e. _V
4 snmapen1
 |-  ( ( (/) e. _V /\ A e. V ) -> ( { (/) } ^m A ) ~~ 1o )
5 3 4 mpan
 |-  ( A e. V -> ( { (/) } ^m A ) ~~ 1o )
6 2 5 eqbrtrid
 |-  ( A e. V -> ( 1o ^m A ) ~~ 1o )