Theorem en1

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004)

	Ref	Expression
Assertion	en1	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
2	1	breq2i	$$⊢A\approx 1_{𝑜}\leftrightarrow A\approx \left\{\varnothing \right\}$$
3		bren	$$⊢A\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
4	2 3	bitri	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
5		f1ocnv	$$⊢f:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A$$
6		f1ofo	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}:\left\{\varnothing \right\}\underset{onto}{⟶}A$$
7		forn	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{onto}{⟶}A\to \mathrm{ran}{f}^{-1}=A$$
8	6 7	syl	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to \mathrm{ran}{f}^{-1}=A$$
9		f1of	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}:\left\{\varnothing \right\}⟶A$$
10		0ex	$$⊢\varnothing \in \mathrm{V}$$
11	10	fsn2	$$⊢f^{-1}:\left\{\varnothing \right\}⟶A\leftrightarrow \left(f^{-1}\left(\varnothing \right)\in A\wedge f^{-1}=\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}\right)$$
12	11	simprbi	$$⊢f^{-1}:\left\{\varnothing \right\}⟶A\to f^{-1}=\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}$$
13	9 12	syl	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}=\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}$$
14	13	rneqd	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to \mathrm{ran}{f}^{-1}=\mathrm{ran}\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}$$
15	10	rnsnop	$$⊢\mathrm{ran}\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
16	14 15	syl6eq	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to \mathrm{ran}{f}^{-1}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
17	8 16	eqtr3d	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to A=\left\{f^{-1}\left(\varnothing \right)\right\}$$
18		fvex	$$⊢f^{-1}\left(\varnothing \right)\in \mathrm{V}$$
19		sneq	$$⊢x=f^{-1}\left(\varnothing \right)\to \left\{x\right\}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
20	19	eqeq2d	$$⊢x=f^{-1}\left(\varnothing \right)\to \left(A=\left\{x\right\}\leftrightarrow A=\left\{f^{-1}\left(\varnothing \right)\right\}\right)$$
21	18 20	spcev	$$⊢A=\left\{f^{-1}\left(\varnothing \right)\right\}\to \exists xA=\left\{x\right\}$$
22	5 17 21	3syl	$$⊢f:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to \exists xA=\left\{x\right\}$$
23	22	exlimiv	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to \exists xA=\left\{x\right\}$$
24	4 23	sylbi	$$⊢A\approx 1_{𝑜}\to \exists xA=\left\{x\right\}$$
25		vex	$$⊢x\in \mathrm{V}$$
26	25	ensn1	$$⊢\left\{x\right\}\approx 1_{𝑜}$$
27		breq1	$$⊢A=\left\{x\right\}\to \left(A\approx 1_{𝑜}\leftrightarrow \left\{x\right\}\approx 1_{𝑜}\right)$$
28	26 27	mpbiri	$$⊢A=\left\{x\right\}\to A\approx 1_{𝑜}$$
29	28	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A\approx 1_{𝑜}$$
30	24 29	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$