Metamath Proof Explorer

Theorem acnnum

Description: A set X which has choice sequences on it of length ~P X is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnnum 
|- ( X e. AC_ ~P X <-> X e. dom card )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( X e. AC_ ~P X -> ~P X e. _V )
2 difss 
 |-  ( ~P X \ { (/) } ) C_ ~P X
3 ssdomg 
 |-  ( ~P X e. _V -> ( ( ~P X \ { (/) } ) C_ ~P X -> ( ~P X \ { (/) } ) ~<_ ~P X ) )
4 1 2 3 mpisyl 
 |-  ( X e. AC_ ~P X -> ( ~P X \ { (/) } ) ~<_ ~P X )
5 acndom 
 |-  ( ( ~P X \ { (/) } ) ~<_ ~P X -> ( X e. AC_ ~P X -> X e. AC_ ( ~P X \ { (/) } ) ) )
6 4 5 mpcom 
 |-  ( X e. AC_ ~P X -> X e. AC_ ( ~P X \ { (/) } ) )
7 eldifsn 
 |-  ( x e. ( ~P X \ { (/) } ) <-> ( x e. ~P X /\ x =/= (/) ) )
8 elpwi 
 |-  ( x e. ~P X -> x C_ X )
9 8 anim1i 
 |-  ( ( x e. ~P X /\ x =/= (/) ) -> ( x C_ X /\ x =/= (/) ) )
10 7 9 sylbi 
 |-  ( x e. ( ~P X \ { (/) } ) -> ( x C_ X /\ x =/= (/) ) )
11 10 rgen 
 |-  A. x e. ( ~P X \ { (/) } ) ( x C_ X /\ x =/= (/) )
12 acni2 
 |-  ( ( X e. AC_ ( ~P X \ { (/) } ) /\ A. x e. ( ~P X \ { (/) } ) ( x C_ X /\ x =/= (/) ) ) -> E. f ( f : ( ~P X \ { (/) } ) --> X /\ A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x ) )
13 6 11 12 sylancl 
 |-  ( X e. AC_ ~P X -> E. f ( f : ( ~P X \ { (/) } ) --> X /\ A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x ) )
14 simpr 
 |-  ( ( f : ( ~P X \ { (/) } ) --> X /\ A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x ) -> A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x )
15 7 imbi1i 
 |-  ( ( x e. ( ~P X \ { (/) } ) -> ( f ` x ) e. x ) <-> ( ( x e. ~P X /\ x =/= (/) ) -> ( f ` x ) e. x ) )
16 impexp 
 |-  ( ( ( x e. ~P X /\ x =/= (/) ) -> ( f ` x ) e. x ) <-> ( x e. ~P X -> ( x =/= (/) -> ( f ` x ) e. x ) ) )
17 15 16 bitri 
 |-  ( ( x e. ( ~P X \ { (/) } ) -> ( f ` x ) e. x ) <-> ( x e. ~P X -> ( x =/= (/) -> ( f ` x ) e. x ) ) )
18 17 ralbii2 
 |-  ( A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x <-> A. x e. ~P X ( x =/= (/) -> ( f ` x ) e. x ) )
19 14 18 sylib 
 |-  ( ( f : ( ~P X \ { (/) } ) --> X /\ A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x ) -> A. x e. ~P X ( x =/= (/) -> ( f ` x ) e. x ) )
20 19 eximi 
 |-  ( E. f ( f : ( ~P X \ { (/) } ) --> X /\ A. x e. ( ~P X \ { (/) } ) ( f ` x ) e. x ) -> E. f A. x e. ~P X ( x =/= (/) -> ( f ` x ) e. x ) )
21 13 20 syl 
 |-  ( X e. AC_ ~P X -> E. f A. x e. ~P X ( x =/= (/) -> ( f ` x ) e. x ) )
22 dfac8a 
 |-  ( X e. AC_ ~P X -> ( E. f A. x e. ~P X ( x =/= (/) -> ( f ` x ) e. x ) -> X e. dom card ) )
23 21 22 mpd 
 |-  ( X e. AC_ ~P X -> X e. dom card )
24 pwexg 
 |-  ( X e. dom card -> ~P X e. _V )
25 numacn 
 |-  ( ~P X e. _V -> ( X e. dom card -> X e. AC_ ~P X ) )
26 24 25 mpcom 
 |-  ( X e. dom card -> X e. AC_ ~P X )
27 23 26 impbii 
 |-  ( X e. AC_ ~P X <-> X e. dom card )