Theorem en1

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

	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		encv	$$⊢A\approx \left\{\varnothing \right\}\to \left(A\in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\right)$$
4		breng	$$⊢\left(A\in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\right)\to \left(A\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\right)$$
5	3 4	syl	$$⊢A\approx \left\{\varnothing \right\}\to \left(A\approx \left\{\varnothing \right\}\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\right)$$
6	5	ibi	$$⊢A\approx \left\{\varnothing \right\}\to \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
7	2 6	sylbi	$$⊢A\approx 1_{𝑜}\to \exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}$$
8		f1ocnv	$$⊢f:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A$$
9		f1ofo	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}:\left\{\varnothing \right\}\underset{onto}{⟶}A$$
10		forn	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{onto}{⟶}A\to \mathrm{ran}{f}^{-1}=A$$
11	9 10	syl	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to \mathrm{ran}{f}^{-1}=A$$
12		f1of	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}:\left\{\varnothing \right\}⟶A$$
13		0ex	$$⊢\varnothing \in \mathrm{V}$$
14	13	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)$$
15	14	simprbi	$$⊢f^{-1}:\left\{\varnothing \right\}⟶A\to f^{-1}=\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}$$
16	12 15	syl	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to f^{-1}=\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}$$
17	16	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\}$$
18	13	rnsnop	$$⊢\mathrm{ran}\left\{⟨\varnothing ,f^{-1}\left(\varnothing \right)⟩\right\}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
19	17 18	eqtrdi	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to \mathrm{ran}{f}^{-1}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
20	11 19	eqtr3d	$$⊢f^{-1}:\left\{\varnothing \right\}\underset{1-1\; onto}{⟶}A\to A=\left\{f^{-1}\left(\varnothing \right)\right\}$$
21		fvex	$$⊢f^{-1}\left(\varnothing \right)\in \mathrm{V}$$
22		sneq	$$⊢x=f^{-1}\left(\varnothing \right)\to \left\{x\right\}=\left\{f^{-1}\left(\varnothing \right)\right\}$$
23	22	eqeq2d	$$⊢x=f^{-1}\left(\varnothing \right)\to \left(A=\left\{x\right\}\leftrightarrow A=\left\{f^{-1}\left(\varnothing \right)\right\}\right)$$
24	21 23	spcev	$$⊢A=\left\{f^{-1}\left(\varnothing \right)\right\}\to \exists xA=\left\{x\right\}$$
25	8 20 24	3syl	$$⊢f:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to \exists xA=\left\{x\right\}$$
26	25	exlimiv	$$⊢\exists ff:A\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\to \exists xA=\left\{x\right\}$$
27	7 26	syl	$$⊢A\approx 1_{𝑜}\to \exists xA=\left\{x\right\}$$
28		vex	$$⊢x\in \mathrm{V}$$
29	28	ensn1	$$⊢\left\{x\right\}\approx 1_{𝑜}$$
30		breq1	$$⊢A=\left\{x\right\}\to \left(A\approx 1_{𝑜}\leftrightarrow \left\{x\right\}\approx 1_{𝑜}\right)$$
31	29 30	mpbiri	$$⊢A=\left\{x\right\}\to A\approx 1_{𝑜}$$
32	31	exlimiv	$$⊢\exists xA=\left\{x\right\}\to A\approx 1_{𝑜}$$
33	27 32	impbii	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$