Metamath Proof Explorer

Theorem acndom2

Description: A set smaller than one with choice sequences of length A also has choice sequences of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acndom2 
|- ( X ~<_ Y -> ( Y e. AC_ A -> X e. AC_ A ) )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( X ~<_ Y -> E. f f : X -1-1-> Y )
2 simplr 
 |-  ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> Y e. AC_ A )
3 imassrn 
 |-  ( f " ( g ` x ) ) C_ ran f
4 simplll 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> f : X -1-1-> Y )
5 f1f 
 |-  ( f : X -1-1-> Y -> f : X --> Y )
6 frn 
 |-  ( f : X --> Y -> ran f C_ Y )
7 4 5 6 3syl 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ran f C_ Y )
8 3 7 sstrid 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( f " ( g ` x ) ) C_ Y )
9 elmapi 
 |-  ( g e. ( ( ~P X \ { (/) } ) ^m A ) -> g : A --> ( ~P X \ { (/) } ) )
10 9 adantl 
 |-  ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> g : A --> ( ~P X \ { (/) } ) )
11 10 ffvelrnda 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( g ` x ) e. ( ~P X \ { (/) } ) )
12 11 eldifad 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( g ` x ) e. ~P X )
13 12 elpwid 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( g ` x ) C_ X )
14 f1dm 
 |-  ( f : X -1-1-> Y -> dom f = X )
15 4 14 syl 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> dom f = X )
16 13 15 sseqtrrd 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( g ` x ) C_ dom f )
17 sseqin2 
 |-  ( ( g ` x ) C_ dom f <-> ( dom f i^i ( g ` x ) ) = ( g ` x ) )
18 16 17 sylib 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( dom f i^i ( g ` x ) ) = ( g ` x ) )
19 eldifsni 
 |-  ( ( g ` x ) e. ( ~P X \ { (/) } ) -> ( g ` x ) =/= (/) )
20 11 19 syl 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( g ` x ) =/= (/) )
21 18 20 eqnetrd 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( dom f i^i ( g ` x ) ) =/= (/) )
22 imadisj 
 |-  ( ( f " ( g ` x ) ) = (/) <-> ( dom f i^i ( g ` x ) ) = (/) )
23 22 necon3bii 
 |-  ( ( f " ( g ` x ) ) =/= (/) <-> ( dom f i^i ( g ` x ) ) =/= (/) )
24 21 23 sylibr 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( f " ( g ` x ) ) =/= (/) )
25 8 24 jca 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ x e. A ) -> ( ( f " ( g ` x ) ) C_ Y /\ ( f " ( g ` x ) ) =/= (/) ) )
26 25 ralrimiva 
 |-  ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> A. x e. A ( ( f " ( g ` x ) ) C_ Y /\ ( f " ( g ` x ) ) =/= (/) ) )
27 acni2 
 |-  ( ( Y e. AC_ A /\ A. x e. A ( ( f " ( g ` x ) ) C_ Y /\ ( f " ( g ` x ) ) =/= (/) ) ) -> E. k ( k : A --> Y /\ A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) ) )
28 2 26 27 syl2anc 
 |-  ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. k ( k : A --> Y /\ A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) ) )
29 acnrcl 
 |-  ( Y e. AC_ A -> A e. _V )
30 29 ad3antlr 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : A --> Y /\ A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> A e. _V )
31 simp-4l 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> f : X -1-1-> Y )
32 f1f1orn 
 |-  ( f : X -1-1-> Y -> f : X -1-1-onto-> ran f )
33 31 32 syl 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> f : X -1-1-onto-> ran f )
34 simprr 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( k ` x ) e. ( f " ( g ` x ) ) )
35 3 34 sselid 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( k ` x ) e. ran f )
36 f1ocnvfv2 
 |-  ( ( f : X -1-1-onto-> ran f /\ ( k ` x ) e. ran f ) -> ( f ` ( `' f ` ( k ` x ) ) ) = ( k ` x ) )
37 33 35 36 syl2anc 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( f ` ( `' f ` ( k ` x ) ) ) = ( k ` x ) )
38 37 34 eqeltrd 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( f ` ( `' f ` ( k ` x ) ) ) e. ( f " ( g ` x ) ) )
39 f1ocnv 
 |-  ( f : X -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> X )
40 f1of 
 |-  ( `' f : ran f -1-1-onto-> X -> `' f : ran f --> X )
41 33 39 40 3syl 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> `' f : ran f --> X )
42 41 35 ffvelrnd 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( `' f ` ( k ` x ) ) e. X )
43 13 ad2ant2r 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( g ` x ) C_ X )
44 f1elima 
 |-  ( ( f : X -1-1-> Y /\ ( `' f ` ( k ` x ) ) e. X /\ ( g ` x ) C_ X ) -> ( ( f ` ( `' f ` ( k ` x ) ) ) e. ( f " ( g ` x ) ) <-> ( `' f ` ( k ` x ) ) e. ( g ` x ) ) )
45 31 42 43 44 syl3anc 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( ( f ` ( `' f ` ( k ` x ) ) ) e. ( f " ( g ` x ) ) <-> ( `' f ` ( k ` x ) ) e. ( g ` x ) ) )
46 38 45 mpbid 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ ( x e. A /\ ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> ( `' f ` ( k ` x ) ) e. ( g ` x ) )
47 46 expr 
 |-  ( ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) /\ x e. A ) -> ( ( k ` x ) e. ( f " ( g ` x ) ) -> ( `' f ` ( k ` x ) ) e. ( g ` x ) ) )
48 47 ralimdva 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : A --> Y ) -> ( A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) -> A. x e. A ( `' f ` ( k ` x ) ) e. ( g ` x ) ) )
49 48 impr 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : A --> Y /\ A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> A. x e. A ( `' f ` ( k ` x ) ) e. ( g ` x ) )
50 acnlem 
 |-  ( ( A e. _V /\ A. x e. A ( `' f ` ( k ` x ) ) e. ( g ` x ) ) -> E. h A. x e. A ( h ` x ) e. ( g ` x ) )
51 30 49 50 syl2anc 
 |-  ( ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : A --> Y /\ A. x e. A ( k ` x ) e. ( f " ( g ` x ) ) ) ) -> E. h A. x e. A ( h ` x ) e. ( g ` x ) )
52 28 51 exlimddv 
 |-  ( ( ( f : X -1-1-> Y /\ Y e. AC_ A ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. h A. x e. A ( h ` x ) e. ( g ` x ) )
53 52 ralrimiva 
 |-  ( ( f : X -1-1-> Y /\ Y e. AC_ A ) -> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. x e. A ( h ` x ) e. ( g ` x ) )
54 vex 
 |-  f e. _V
55 54 dmex 
 |-  dom f e. _V
56 14 55 eqeltrrdi 
 |-  ( f : X -1-1-> Y -> X e. _V )
57 isacn 
 |-  ( ( X e. _V /\ A e. _V ) -> ( X e. AC_ A <-> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. x e. A ( h ` x ) e. ( g ` x ) ) )
58 56 29 57 syl2an 
 |-  ( ( f : X -1-1-> Y /\ Y e. AC_ A ) -> ( X e. AC_ A <-> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. x e. A ( h ` x ) e. ( g ` x ) ) )
59 53 58 mpbird 
 |-  ( ( f : X -1-1-> Y /\ Y e. AC_ A ) -> X e. AC_ A )
60 59 ex 
 |-  ( f : X -1-1-> Y -> ( Y e. AC_ A -> X e. AC_ A ) )
61 60 exlimiv 
 |-  ( E. f f : X -1-1-> Y -> ( Y e. AC_ A -> X e. AC_ A ) )
62 1 61 syl 
 |-  ( X ~<_ Y -> ( Y e. AC_ A -> X e. AC_ A ) )