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 ) )