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\in V\to \left({1_{𝑜}}^A\right)\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2	1	oveq1i	$$⊢{1_{𝑜}}^A={\left\{\varnothing \right\}}^A$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		snmapen1	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in V\right)\to \left({\left\{\varnothing \right\}}^A\right)\approx 1_{𝑜}$$
5	3 4	mpan	$$⊢A\in V\to \left({\left\{\varnothing \right\}}^A\right)\approx 1_{𝑜}$$
6	2 5	eqbrtrid	$$⊢A\in V\to \left({1_{𝑜}}^A\right)\approx 1_{𝑜}$$