Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002)

	Ref	Expression
Hypothesis	ensn1.1	$$⊢A\in \mathrm{V}$$
Assertion	ensn1	$$⊢\left\{A\right\}\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		ensn1.1	$$⊢A\in \mathrm{V}$$
2		snex	$$⊢\left\{⟨A,\varnothing ⟩\right\}\in \mathrm{V}$$
3		f1oeq1	$$⊢f=\left\{⟨A,\varnothing ⟩\right\}\to \left(f:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\leftrightarrow \left\{⟨A,\varnothing ⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\right)$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	1 4	f1osn	$$⊢\left\{⟨A,\varnothing ⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
6	2 3 5	ceqsexv2d	$$⊢\exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
7		bren	$$⊢\left\{A\right\}\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
8	6 7	mpbir	$$⊢\left\{A\right\}\approx \left\{\varnothing \right\}$$
9		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
10	8 9	breqtrri	$$⊢\left\{A\right\}\approx 1_{𝑜}$$