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

Proof

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