This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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