Theorem ween

Description: A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	ween	|- ( A e. dom card <-> E. r r We A )

Proof

Step	Hyp	Ref	Expression
1		dfac8b	|- ( A e. dom card -> E. r r We A )
2		weso	|- ( r We A -> r Or A )
3		vex	|- r e. _V
4		soex	|- ( ( r Or A /\ r e. _V ) -> A e. _V )
5	2 3 4	sylancl	|- ( r We A -> A e. _V )
6	5	exlimiv	|- ( E. r r We A -> A e. _V )
7		unipw	|- U. ~P A = A
8		weeq2	|- ( U. ~P A = A -> ( r We U. ~P A <-> r We A ) )
9	7 8	ax-mp	|- ( r We U. ~P A <-> r We A )
10	9	exbii	|- ( E. r r We U. ~P A <-> E. r r We A )
11	10	biimpri	|- ( E. r r We A -> E. r r We U. ~P A )
12		pwexg	|- ( A e. _V -> ~P A e. _V )
13		dfac8c	|- ( ~P A e. _V -> ( E. r r We U. ~P A -> E. f A. x e. ~P A ( x =/= (/) -> ( f ` x ) e. x ) ) )
14	12 13	syl	|- ( A e. _V -> ( E. r r We U. ~P A -> E. f A. x e. ~P A ( x =/= (/) -> ( f ` x ) e. x ) ) )
15		dfac8a	|- ( A e. _V -> ( E. f A. x e. ~P A ( x =/= (/) -> ( f ` x ) e. x ) -> A e. dom card ) )
16	14 15	syld	|- ( A e. _V -> ( E. r r We U. ~P A -> A e. dom card ) )
17	6 11 16	sylc	|- ( E. r r We A -> A e. dom card )
18	1 17	impbii	|- ( A e. dom card <-> E. r r We A )