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 V 1 𝑜 A 1 𝑜

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 1 oveq1i 1 𝑜 A = A
3 0ex V
4 snmapen1 V A V A 1 𝑜
5 3 4 mpan A V A 1 𝑜
6 2 5 eqbrtrid A V 1 𝑜 A 1 𝑜