MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  acndom Unicode version
Theorem acndom 7896
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.)
Assertion
Ref Expression
acndom |- ( A ~<_ B -> ( X e. AC B -> X e. AC A ) )
Proof of Theorem acndom
Dummy variables f g h k x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdomi 7086 . 2 |- ( A ~<_ B -> E. f f : A -1-1-> B )
2 neq0 3606 . . . . 5 |- ( -. A = (/) <-> E. x x e. A )
3 simpl3 962 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> X e. AC B )
4 elmapi 7005 . . . . . . . . . . . . . . 15 |- ( g e. ( ( ~P X \ { (/) } ) ^m A ) -> g : A --> ( ~P X \ { (/) } ) )
54ad2antlr 708 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 996 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 5652 . . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-> B -> f : A -1-1-onto-> ran f )
86, 7syl 16 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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-onto-> ran f )
9 f1ocnv 5654 . . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> A )
10 f1of 5641 . . . . . . . . . . . . . . . . 17 |- ( `' f : ran f -1-1-onto-> A -> `' f : ran f --> A )
118, 9, 103syl 19 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
1211ffvelrnda 5837 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 )
13 simpl2 961 . . . . . . . . . . . . . . . 16 |- ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) -> x e. A )
1413ad2antrr 707 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 )
1512, 14ifclda 3734 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
165, 15ffvelrnd 5838 . . . . . . . . . . . . 13 |- ( ( ( ( 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 \ { (/) } ) )
17 eldifsn 3895 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) =/= (/) ) )
18 elpwi 3775 . . . . . . . . . . . . . . 15 |- ( ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) e. ~P X -> ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) C_ X )
1918anim1i 552 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) =/= (/) ) )
2017, 19sylbi 188 . . . . . . . . . . . . 13 |- ( ( 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 ) ) =/= (/) ) )
2116, 20syl 16 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) =/= (/) ) )
2221ralrimiva 2757 . . . . . . . . . . 11 |- ( ( ( 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 ) ) =/= (/) ) )
23 acni2 7891 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
243, 22, 23syl2anc 643 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
25 f1dm 5610 . . . . . . . . . . . . . 14 |- ( f : A -1-1-> B -> dom f = A )
26 vex 2927 . . . . . . . . . . . . . . 15 |- f e. _V
2726dmex 5099 . . . . . . . . . . . . . 14 |- dom f e. _V
2825, 27syl6eqelr 2501 . . . . . . . . . . . . 13 |- ( f : A -1-1-> B -> A e. _V )
29283ad2ant1 978 . . . . . . . . . . . 12 |- ( ( f : A -1-1-> B /\ x e. A /\ X e. AC B ) -> A e. _V )
3029ad2antrr 707 . . . . . . . . . . 11 |- ( ( ( ( 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 )
31 simpll1 996 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
32 f1f 5606 . . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-> B -> f : A --> B )
33 frn 5564 . . . . . . . . . . . . . . . . 17 |- ( f : A --> B -> ran f C_ B )
3431, 32, 333syl 19 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-> B /\ x e. A /\ X e. AC B ) /\ g e. ( ( ~P X \ { (/) } ) ^m A ) ) /\ k : B --> X ) -> ran f C_ B )
35 ssralv 3375 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
3634, 35syl 16 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) )
37 iftrue 3713 . . . . . . . . . . . . . . . . . 18 |- ( y e. ran f -> if ( y e. ran f , ( `' f ` y ) , x ) = ( `' f ` y ) )
3837fveq2d 5699 . . . . . . . . . . . . . . . . 17 |- ( y e. ran f -> ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) = ( g ` ( `' f ` y ) ) )
3938eleq2d 2479 . . . . . . . . . . . . . . . 16 |- ( y e. ran f -> ( ( k ` y ) e. ( g ` if ( y e. ran f , ( `' f ` y ) , x ) ) <-> ( k ` y ) e. ( g ` ( `' f ` y ) ) ) )
4039ralbiia 2706 . . . . . . . . . . . . . . 15 |- ( 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 ) ) )
4136, 40syl6ib 218 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) )
42 f1fn 5607 . . . . . . . . . . . . . . 15 |- ( f : A -1-1-> B -> f Fn A )
43 fveq2 5695 . . . . . . . . . . . . . . . . 17 |- ( y = ( f ` z ) -> ( k ` y ) = ( k ` ( f ` z ) ) )
44 fveq2 5695 . . . . . . . . . . . . . . . . . 18 |- ( y = ( f ` z ) -> ( `' f ` y ) = ( `' f ` ( f ` z ) ) )
4544fveq2d 5699 . . . . . . . . . . . . . . . . 17 |- ( y = ( f ` z ) -> ( g ` ( `' f ` y ) ) = ( g ` ( `' f ` ( f ` z ) ) ) )
4643, 45eleq12d 2480 . . . . . . . . . . . . . . . 16 |- ( y = ( f ` z ) -> ( ( k ` y ) e. ( g ` ( `' f ` y ) ) <-> ( k ` ( f ` z ) ) e. ( g ` ( `' f ` ( f ` z ) ) ) ) )
4746ralrn 5840 . . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
4831, 42, 473syl 19 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) ) )
4941, 48sylibd 206 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) ) )
5031, 7syl 16 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
51 f1ocnvfv1 5981 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-onto-> ran f /\ z e. A ) -> ( `' f ` ( f ` z ) ) = z )
5250, 51sylan 458 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 )
5352fveq2d 5699 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) )
5453eleq2d 2479 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) ) )
5554ralbidva 2690 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
5649, 55sylibd 206 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
5756impr 603 . . . . . . . . . . 11 |- ( ( ( ( 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 ) )
58 acnlem 7893 . . . . . . . . . . 11 |- ( ( A e. _V /\ A. z e. A ( k ` ( f ` z ) ) e. ( g ` z ) ) -> E. h A. z e. A ( h ` z ) e. ( g ` z ) )
5930, 57, 58syl2anc 643 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
6024, 59exlimddv 1645 . . . . . . . . 9 |- ( ( ( 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 ) )
6160ralrimiva 2757 . . . . . . . 8 |- ( ( 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 ) )
62 elex 2932 . . . . . . . . . 10 |- ( X e. AC B -> X e. _V )
63 isacn 7889 . . . . . . . . . 10 |- ( ( 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 ) ) )
6462, 28, 63syl2anr 465 . . . . . . . . 9 |- ( ( 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 ) ) )
65643adant2 976 . . . . . . . 8 |- ( ( 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 ) ) )
6661, 65mpbird 224 . . . . . . 7 |- ( ( f : A -1-1-> B /\ x e. A /\ X e. AC B ) -> X e. AC A )
67663exp 1152 . . . . . 6 |- ( f : A -1-1-> B -> ( x e. A -> ( X e. AC B -> X e. AC A ) ) )
6867exlimdv 1643 . . . . 5 |- ( f : A -1-1-> B -> ( E. x x e. A -> ( X e. AC B -> X e. AC A ) ) )
692, 68syl5bi 209 . . . 4 |- ( f : A -1-1-> B -> ( -. A = (/) -> ( X e. AC B -> X e. AC A ) ) )
70 acneq 7888 . . . . . . 7 |- ( A = (/) -> AC A = AC (/) )
71 0fin 7303 . . . . . . . 8 |- (/) e. Fin
72 finacn 7895 . . . . . . . 8 |- ( (/) e. Fin -> AC (/) = _V )
7371, 72ax-mp 8 . . . . . . 7 |- AC (/) = _V
7470, 73syl6eq 2460 . . . . . 6 |- ( A = (/) -> AC A = _V )
7574eleq2d 2479 . . . . 5 |- ( A = (/) -> ( X e. AC A <-> X e. _V ) )
7662, 75syl5ibr 213 . . . 4 |- ( A = (/) -> ( X e. AC B -> X e. AC A ) )
7769, 76pm2.61d2 154 . . 3 |- ( f : A -1-1-> B -> ( X e. AC B -> X e. AC A ) )
7877exlimiv 1641 . 2 |- ( E. f f : A -1-1-> B -> ( X e. AC B -> X e. AC A ) )
791, 78syl 16 1 |- ( A ~<_ B -> ( X e. AC B -> X e. AC A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   =/= wne 2575   A.wral 2674   _Vcvv 2924   \ cdif 3285   C_ wss 3288   (/)c0 3596   ifcif 3707   ~Pcpw 3767   {csn 3782   class class class wbr 4180   `'ccnv 4844   dom cdm 4845   ran crn 4846   Fn wfn 5416   -->wf 5417   -1-1->wf1 5418   -1-1-onto->wf1o 5420   ` cfv 5421  (class class class)co 6048   ^m cmap 6985   ~<_ cdom 7074   Fincfn 7076  AC wacn 7789
This theorem is referenced by:  acnnum  7897  acnen  7898  iunctb  8413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-1o 6691  df-er 6872  df-map 6987  df-en 7077  df-dom 7078  df-fin 7080  df-acn 7793
  Copyright terms: Public domain W3C validator