Metamath Proof Explorer

Theorem acndom

Description: A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )
2 neq0 
 |-  ( -. A = (/) <-> E. x x e. A )
3 simpl3 
 |-  ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> X e. AC_ B )
4 elmapi 
 |-  ( g e. ( ( ~P X \ { (/) } ) ^m A ) -> g : A --> ( ~P X \ { (/) } ) )
5 4 ad2antlr 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> g : A --> ( ~P X \ { (/) } ) )
6 simpll1 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> f : A -1-1-> B )
7 f1f1orn 
 |-  ( f : A -1-1-> B -> f : A -1-1-onto-> ran f )
8 f1ocnv 
 |-  ( f : A -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> A )
9 f1of 
 |-  ( `' f : ran f -1-1-onto-> A -> `' f : ran f --> A )
10 6 7 8 9 4syl 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> `' f : ran f --> A )
11 10 ffvelcdmda 
 |-  ( ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) /\ y e. ran f ) -> ( `' f ` y ) e. A )
12 simpl2 
 |-  ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> x e. A )
13 12 ad2antrr 
 |-  ( ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) /\ -. y e. ran f ) -> x e. A )
14 11 13 ifclda 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> if ( y e. ran f , ( `' f ` y ) , x ) e. A )
15 5 14 ffvelcdmd 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ( ~P X \ { (/) } ) )
16 eldifsn 
 |-  ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ( ~P X \ { (/) } ) <-> ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ~P X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) )
17 elpwi 
 |-  ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ~P X -> ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X )
18 17 anim1i 
 |-  ( ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ~P X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) -> ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) )
19 16 18 sylbi 
 |-  ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ( ~P X \ { (/) } ) -> ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) )
20 15 19 syl 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ y e. B ) -> ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) )
21 20 ralrimiva 
 |-  ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> A. y e. B ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) )
22 acni2 
 |-  ( ( X e. AC_ B /\ A. y e. B ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X /\ ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) =/= (/) ) ) -> E. k ( k : B --> X /\ A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) )
23 3 21 22 syl2anc 
 |-  ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. k ( k : B --> X /\ A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) )
24 f1dm 
 |-  ( f : A -1-1-> B -> dom f = A )
25 vex 
 |-  f e. _V
26 25 dmex 
 |-  dom f e. _V
27 24 26 eqeltrrdi 
 |-  ( f : A -1-1-> B -> A e. _V )
28 27 3ad2ant1 
 |-  ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) -> A e. _V )
29 28 ad2antrr 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : B --> X /\ A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) ) -> A e. _V )
30 simpll1 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> f : A -1-1-> B )
31 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
32 frn 
 |-  ( f : A --> B -> ran f C_ B )
33 ssralv 
 |-  ( ran f C_ B -> ( A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) -> A. y e. ran f ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) )
34 30 31 32 33 4syl 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) -> A. y e. ran f ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) )
35 iftrue 
 |-  ( y e. ran f -> if ( y e. ran f , ( `' f ` y ) , x ) = ( `' f ` y ) )
36 35 fveq2d 
 |-  ( y e. ran f -> ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) = ( g ` ( `' f ` y ) ) )
37 36 eleq2d 
 |-  ( y e. ran f -> ( ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) <-> ( k ` y ) e. ( g ` ( `' f ` y ) ) ) )
38 37 ralbiia 
 |-  ( A. y e. ran f ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) <-> A. y e. ran f ( k ` y ) e. ( g ` ( `' f ` y ) ) )
39 34 38 imbitrdi 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) -> A. y e. ran f ( k ` y ) e. ( g ` ( `' f ` y ) ) ) )
40 f1fn 
 |-  ( f : A -1-1-> B -> f Fn A )
41 fveq2 
 |-  ( y = ( f ` z ) -> ( k ` y ) = ( k ` ( f ` z ) ) )
42 2fveq3 
 |-  ( y = ( f ` z ) -> ( g ` ( `' f ` y ) ) = ( g ` ( `' f ` ( f ` z ) ) ) )
43 41 42 eleq12d 
 |-  ( y = ( f ` z ) -> ( ( k ` y ) e. ( g ` ( `' f ` y ) ) <-> ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) ) )
44 43 ralrn 
 |-  ( f Fn A -> ( A. y e. ran f ( k ` y ) e. ( g ` ( `' f ` y ) ) <-> A. z e. A ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) ) )
45 30 40 44 3syl 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. y e. ran f ( k ` y ) e. ( g ` ( `' f ` y ) ) <-> A. z e. A ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) ) )
46 39 45 sylibd 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) -> A. z e. A ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) ) )
47 30 7 syl 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> f : A -1-1-onto-> ran f )
48 f1ocnvfv1 
 |-  ( ( f : A -1-1-onto-> ran f /\ z e. A ) -> ( `' f ` ( f ` z ) ) = z )
49 47 48 sylan 
 |-  ( ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) /\ z e. A ) -> ( `' f ` ( f ` z ) ) = z )
50 49 fveq2d 
 |-  ( ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) /\ z e. A ) -> ( g ` ( `' f ` ( f ` z ) ) ) = ( g ` z ) )
51 50 eleq2d 
 |-  ( ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) /\ z e. A ) -> ( ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) <-> ( k ` ( f ` z ) ) e. ( g ` z ) ) )
52 51 ralbidva 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. z e. A ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) <-> A. z e. A ( k ` ( f ` z ) ) e. ( g ` z ) ) )
53 46 52 sylibd 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ( A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) -> A. z e. A ( k ` ( f ` z ) ) e. ( g ` z ) ) )
54 53 impr 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : B --> X /\ A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) ) -> A. z e. A ( k ` ( f ` z ) ) e. ( g ` z ) )
55 acnlem 
 |-  ( ( A e. _V /\ A. z e. A ( k ` ( f ` z ) ) e. ( g ` z ) ) -> E. h A. z e. A ( h ` z ) e. ( g ` z ) )
56 29 54 55 syl2anc 
 |-  ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ ( k : B --> X /\ A. y e. B ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) ) ) -> E. h A. z e. A ( h ` z ) e. ( g ` z ) )
57 23 56 exlimddv 
 |-  ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> E. h A. z e. A ( h ` z ) e. ( g ` z ) )
58 57 ralrimiva 
 |-  ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) -> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. z e. A ( h ` z ) e. ( g ` z ) )
59 elex 
 |-  ( X e. AC_ B -> X e. _V )
60 isacn 
 |-  ( ( X e. _V /\ A e. _V ) -> ( X e. AC_ A <-> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. z e. A ( h ` z ) e. ( g ` z ) ) )
61 59 27 60 syl2anr 
 |-  ( ( f : A -1-1-> B /\ X e. AC_ B ) -> ( X e. AC_ A <-> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. z e. A ( h ` z ) e. ( g ` z ) ) )
62 61 3adant2 
 |-  ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) -> ( X e. AC_ A <-> A. g e. ( ( ~P X \ { (/) } ) ^m A ) E. h A. z e. A ( h ` z ) e. ( g ` z ) ) )
63 58 62 mpbird 
 |-  ( ( f : A -1-1-> B /\ x e. A /\ X e. AC_ B ) -> X e. AC_ A )
64 63 3exp 
 |-  ( f : A -1-1-> B -> ( x e. A -> ( X e. AC_ B -> X e. AC_ A ) ) )
65 64 exlimdv 
 |-  ( f : A -1-1-> B -> ( E. x x e. A -> ( X e. AC_ B -> X e. AC_ A ) ) )
66 2 65 biimtrid 
 |-  ( f : A -1-1-> B -> ( -. A = (/) -> ( X e. AC_ B -> X e. AC_ A ) ) )
67 acneq 
 |-  ( A = (/) -> AC_ A = AC_ (/) )
68 0fi 
 |-  (/) e. Fin
69 finacn 
 |-  ( (/) e. Fin -> AC_ (/) = _V )
70 68 69 ax-mp 
 |-  AC_ (/) = _V
71 67 70 eqtrdi 
 |-  ( A = (/) -> AC_ A = _V )
72 71 eleq2d 
 |-  ( A = (/) -> ( X e. AC_ A <-> X e. _V ) )
73 59 72 imbitrrid 
 |-  ( A = (/) -> ( X e. AC_ B -> X e. AC_ A ) )
74 66 73 pm2.61d2 
 |-  ( f : A -1-1-> B -> ( X e. AC_ B -> X e. AC_ A ) )
75 74 exlimiv 
 |-  ( E. f f : A -1-1-> B -> ( X e. AC_ B -> X e. AC_ A ) )
76 1 75 syl 
 |-  ( A ~<_ B -> ( X e. AC_ B -> X e. AC_ A ) )