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 e. _V
Assertion	ensn1	|- { A } ~~ 1o

Proof

Step	Hyp	Ref	Expression
1		ensn1.1	|- A e. _V
2		snex	|- { <. A , (/) >. } e. _V
3		f1oeq1	|- ( f = { <. A , (/) >. } -> ( f : { A } -1-1-onto-> { (/) } <-> { <. A , (/) >. } : { A } -1-1-onto-> { (/) } ) )
4		0ex	|- (/) e. _V
5	1 4	f1osn	|- { <. A , (/) >. } : { A } -1-1-onto-> { (/) }
6	2 3 5	ceqsexv2d	|- E. f f : { A } -1-1-onto-> { (/) }
7		snex	|- { A } e. _V
8		snex	|- { (/) } e. _V
9		breng	|- ( ( { A } e. _V /\ { (/) } e. _V ) -> ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } ) )
10	7 8 9	mp2an	|- ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } )
11	6 10	mpbir	|- { A } ~~ { (/) }
12		df1o2	|- 1o = { (/) }
13	11 12	breqtrri	|- { A } ~~ 1o