Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

	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		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
8		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
9		breng	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\right)\to \left(\left\{A\right\}\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\right)$$
10	7 8 9	mp2an	$$⊢\left\{A\right\}\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
11	6 10	mpbir	$$⊢\left\{A\right\}\approx \left\{\varnothing \right\}$$
12		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
13	11 12	breqtrri	$$⊢\left\{A\right\}\approx 1_{𝑜}$$