Metamath Proof Explorer

Theorem numacn

Description: A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion numacn 
|- ( A e. V -> ( X e. dom card -> X e. AC_ A ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 simpll 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> X e. dom card )
3 elmapi 
 |-  ( f e. ( ( ~P X \ { (/) } ) ^m A ) -> f : A --> ( ~P X \ { (/) } ) )
4 3 adantl 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> f : A --> ( ~P X \ { (/) } ) )
5 4 frnd 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> ran f C_ ( ~P X \ { (/) } ) )
6 5 difss2d 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> ran f C_ ~P X )
7 sspwuni 
 |-  ( ran f C_ ~P X <-> U. ran f C_ X )
8 6 7 sylib 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> U. ran f C_ X )
9 ssnum 
 |-  ( ( X e. dom card /\ U. ran f C_ X ) -> U. ran f e. dom card )
10 2 8 9 syl2anc 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> U. ran f e. dom card )
11 ssdifin0 
 |-  ( ran f C_ ( ~P X \ { (/) } ) -> ( ran f i^i { (/) } ) = (/) )
12 5 11 syl 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> ( ran f i^i { (/) } ) = (/) )
13 disjsn 
 |-  ( ( ran f i^i { (/) } ) = (/) <-> -. (/) e. ran f )
14 12 13 sylib 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> -. (/) e. ran f )
15 ac5num 
 |-  ( ( U. ran f e. dom card /\ -. (/) e. ran f ) -> E. h ( h : ran f --> U. ran f /\ A. y e. ran f ( h ` y ) e. y ) )
16 10 14 15 syl2anc 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. h ( h : ran f --> U. ran f /\ A. y e. ran f ( h ` y ) e. y ) )
17 simpllr 
 |-  ( ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( h : ran f --> U. ran f /\ A. y e. ran f ( h ` y ) e. y ) ) -> A e. _V )
18 4 ffnd 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> f Fn A )
19 fveq2 
 |-  ( y = ( f ` x ) -> ( h ` y ) = ( h ` ( f ` x ) ) )
20 id 
 |-  ( y = ( f ` x ) -> y = ( f ` x ) )
21 19 20 eleq12d 
 |-  ( y = ( f ` x ) -> ( ( h ` y ) e. y <-> ( h ` ( f ` x ) ) e. ( f ` x ) ) )
22 21 ralrn 
 |-  ( f Fn A -> ( A. y e. ran f ( h ` y ) e. y <-> A. x e. A ( h ` ( f ` x ) ) e. ( f ` x ) ) )
23 18 22 syl 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> ( A. y e. ran f ( h ` y ) e. y <-> A. x e. A ( h ` ( f ` x ) ) e. ( f ` x ) ) )
24 23 biimpa 
 |-  ( ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ A. y e. ran f ( h ` y ) e. y ) -> A. x e. A ( h ` ( f ` x ) ) e. ( f ` x ) )
25 24 adantrl 
 |-  ( ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( h : ran f --> U. ran f /\ A. y e. ran f ( h ` y ) e. y ) ) -> A. x e. A ( h ` ( f ` x ) ) e. ( f ` x ) )
26 acnlem 
 |-  ( ( A e. _V /\ A. x e. A ( h ` ( f ` x ) ) e. ( f ` x ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) )
27 17 25 26 syl2anc 
 |-  ( ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( h : ran f --> U. ran f /\ A. y e. ran f ( h ` y ) e. y ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) )
28 16 27 exlimddv 
 |-  ( ( ( X e. dom card /\ A e. _V ) /\ f e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) )
29 28 ralrimiva 
 |-  ( ( X e. dom card /\ A e. _V ) -> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) )
30 isacn 
 |-  ( ( X e. dom card /\ A e. _V ) -> ( X e. AC_ A <-> A. f e. ( ( ~P X \ { (/) } ) ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) ) )
31 29 30 mpbird 
 |-  ( ( X e. dom card /\ A e. _V ) -> X e. AC_ A )
32 31 expcom 
 |-  ( A e. _V -> ( X e. dom card -> X e. AC_ A ) )
33 1 32 syl 
 |-  ( A e. V -> ( X e. dom card -> X e. AC_ A ) )