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	⊢ ( 𝐴 ∈ 𝑉 → ( 1o ↑m 𝐴 ) ≈ 1o )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	oveq1i	⊢ ( 1o ↑m 𝐴 ) = ( { ∅ } ↑m 𝐴 )
3		0ex	⊢ ∅ ∈ V
4		snmapen1	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } ↑m 𝐴 ) ≈ 1o )
5	3 4	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } ↑m 𝐴 ) ≈ 1o )
6	2 5	eqbrtrid	⊢ ( 𝐴 ∈ 𝑉 → ( 1o ↑m 𝐴 ) ≈ 1o )