Metamath Proof Explorer


Theorem map0e

Description: Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of Mendelson p. 255. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 14-Jul-2022)

Ref Expression
Assertion map0e ( 𝐴𝑉 → ( 𝐴m ∅ ) = 1o )

Proof

Step Hyp Ref Expression
1 mapdm0 ( 𝐴𝑉 → ( 𝐴m ∅ ) = { ∅ } )
2 df1o2 1o = { ∅ }
3 1 2 eqtr4di ( 𝐴𝑉 → ( 𝐴m ∅ ) = 1o )