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 )