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 ~~ 1o <-> E. x A = { x } )

Proof

Step	Hyp	Ref	Expression
1		df1o2	|- 1o = { (/) }
2	1	breq2i	|- ( A ~~ 1o <-> A ~~ { (/) } )
3		encv	|- ( A ~~ { (/) } -> ( A e. _V /\ { (/) } e. _V ) )
4		breng	|- ( ( A e. _V /\ { (/) } e. _V ) -> ( A ~~ { (/) } <-> E. f f : A -1-1-onto-> { (/) } ) )
5	3 4	syl	|- ( A ~~ { (/) } -> ( A ~~ { (/) } <-> E. f f : A -1-1-onto-> { (/) } ) )
6	5	ibi	|- ( A ~~ { (/) } -> E. f f : A -1-1-onto-> { (/) } )
7	2 6	sylbi	|- ( A ~~ 1o -> E. f f : A -1-1-onto-> { (/) } )
8		f1ocnv	|- ( f : A -1-1-onto-> { (/) } -> `' f : { (/) } -1-1-onto-> A )
9		f1ofo	|- ( `' f : { (/) } -1-1-onto-> A -> `' f : { (/) } -onto-> A )
10		forn	|- ( `' f : { (/) } -onto-> A -> ran `' f = A )
11	9 10	syl	|- ( `' f : { (/) } -1-1-onto-> A -> ran `' f = A )
12		f1of	|- ( `' f : { (/) } -1-1-onto-> A -> `' f : { (/) } --> A )
13		0ex	|- (/) e. _V
14	13	fsn2	|- ( `' f : { (/) } --> A <-> ( ( `' f ` (/) ) e. A /\ `' f = { <. (/) , ( `' f ` (/) ) >. } ) )
15	14	simprbi	|- ( `' f : { (/) } --> A -> `' f = { <. (/) , ( `' f ` (/) ) >. } )
16	12 15	syl	|- ( `' f : { (/) } -1-1-onto-> A -> `' f = { <. (/) , ( `' f ` (/) ) >. } )
17	16	rneqd	|- ( `' f : { (/) } -1-1-onto-> A -> ran `' f = ran { <. (/) , ( `' f ` (/) ) >. } )
18	13	rnsnop	|- ran { <. (/) , ( `' f ` (/) ) >. } = { ( `' f ` (/) ) }
19	17 18	eqtrdi	|- ( `' f : { (/) } -1-1-onto-> A -> ran `' f = { ( `' f ` (/) ) } )
20	11 19	eqtr3d	|- ( `' f : { (/) } -1-1-onto-> A -> A = { ( `' f ` (/) ) } )
21		fvex	|- ( `' f ` (/) ) e. _V
22		sneq	|- ( x = ( `' f ` (/) ) -> { x } = { ( `' f ` (/) ) } )
23	22	eqeq2d	|- ( x = ( `' f ` (/) ) -> ( A = { x } <-> A = { ( `' f ` (/) ) } ) )
24	21 23	spcev	|- ( A = { ( `' f ` (/) ) } -> E. x A = { x } )
25	8 20 24	3syl	|- ( f : A -1-1-onto-> { (/) } -> E. x A = { x } )
26	25	exlimiv	|- ( E. f f : A -1-1-onto-> { (/) } -> E. x A = { x } )
27	7 26	syl	|- ( A ~~ 1o -> E. x A = { x } )
28		vex	|- x e. _V
29	28	ensn1	|- { x } ~~ 1o
30		breq1	|- ( A = { x } -> ( A ~~ 1o <-> { x } ~~ 1o ) )
31	29 30	mpbiri	|- ( A = { x } -> A ~~ 1o )
32	31	exlimiv	|- ( E. x A = { x } -> A ~~ 1o )
33	27 32	impbii	|- ( A ~~ 1o <-> E. x A = { x } )