Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Assertion	en1b	|- ( A ~~ 1o <-> A = { U. A } )

Proof

Step	Hyp	Ref	Expression
1		en1	|- ( A ~~ 1o <-> E. x A = { x } )
2		id	|- ( A = { x } -> A = { x } )
3		unieq	|- ( A = { x } -> U. A = U. { x } )
4		vex	|- x e. _V
5	4	unisn	|- U. { x } = x
6	3 5	eqtrdi	|- ( A = { x } -> U. A = x )
7	6	sneqd	|- ( A = { x } -> { U. A } = { x } )
8	2 7	eqtr4d	|- ( A = { x } -> A = { U. A } )
9	8	exlimiv	|- ( E. x A = { x } -> A = { U. A } )
10	1 9	sylbi	|- ( A ~~ 1o -> A = { U. A } )
11		id	|- ( A = { U. A } -> A = { U. A } )
12		snex	|- { U. A } e. _V
13	11 12	eqeltrdi	|- ( A = { U. A } -> A e. _V )
14	13	uniexd	|- ( A = { U. A } -> U. A e. _V )
15		ensn1g	|- ( U. A e. _V -> { U. A } ~~ 1o )
16	14 15	syl	|- ( A = { U. A } -> { U. A } ~~ 1o )
17	11 16	eqbrtrd	|- ( A = { U. A } -> A ~~ 1o )
18	10 17	impbii	|- ( A ~~ 1o <-> A = { U. A } )