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∈AC_B→X∈AC_A

Proof

Step Hyp Ref Expression
1 brdomi ⊢A≼B→∃ff:A⟶1-1B
2 neq0 ⊢¬A=∅↔∃xx∈A
3 simpl3 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A→X∈AC_B
4 elmapi ⊢g∈𝒫X∖∅A→g:A⟶𝒫X∖∅
5 4 ad2antlr ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→g:A⟶𝒫X∖∅
6 simpll1 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→f:A⟶1-1B
7 f1f1orn ⊢f:A⟶1-1B→f:A⟶1-1 ontoran⁡f
8 f1ocnv ⊢f:A⟶1-1 ontoran⁡f→f-1:ran⁡f⟶1-1 ontoA
9 f1of ⊢f-1:ran⁡f⟶1-1 ontoA→f-1:ran⁡f⟶A
10 6 7 8 9 4syl ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→f-1:ran⁡f⟶A
11 10 ffvelcdmda ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B∧y∈ran⁡f→f-1⁡y∈A
12 simpl2 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A→x∈A
13 12 ad2antrr ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B∧¬y∈ran⁡f→x∈A
14 11 13 ifclda ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→ify∈ran⁡ff-1⁡yx∈A
15 5 14 ffvelcdmd ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→g⁡ify∈ran⁡ff-1⁡yx∈𝒫X∖∅
16 eldifsn ⊢g⁡ify∈ran⁡ff-1⁡yx∈𝒫X∖∅↔g⁡ify∈ran⁡ff-1⁡yx∈𝒫X∧g⁡ify∈ran⁡ff-1⁡yx≠∅
17 elpwi ⊢g⁡ify∈ran⁡ff-1⁡yx∈𝒫X→g⁡ify∈ran⁡ff-1⁡yx⊆X
18 17 anim1i ⊢g⁡ify∈ran⁡ff-1⁡yx∈𝒫X∧g⁡ify∈ran⁡ff-1⁡yx≠∅→g⁡ify∈ran⁡ff-1⁡yx⊆X∧g⁡ify∈ran⁡ff-1⁡yx≠∅
19 16 18 sylbi ⊢g⁡ify∈ran⁡ff-1⁡yx∈𝒫X∖∅→g⁡ify∈ran⁡ff-1⁡yx⊆X∧g⁡ify∈ran⁡ff-1⁡yx≠∅
20 15 19 syl ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧y∈B→g⁡ify∈ran⁡ff-1⁡yx⊆X∧g⁡ify∈ran⁡ff-1⁡yx≠∅
21 20 ralrimiva ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A→∀y∈Bg⁡ify∈ran⁡ff-1⁡yx⊆X∧g⁡ify∈ran⁡ff-1⁡yx≠∅
22 acni2 ⊢X∈AC_B∧∀y∈Bg⁡ify∈ran⁡ff-1⁡yx⊆X∧g⁡ify∈ran⁡ff-1⁡yx≠∅→∃kk:B⟶X∧∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx
23 3 21 22 syl2anc ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A→∃kk:B⟶X∧∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx
24 f1dm ⊢f:A⟶1-1B→dom⁡f=A
25 vex ⊢f∈V
26 25 dmex ⊢dom⁡f∈V
27 24 26 eqeltrrdi ⊢f:A⟶1-1B→A∈V
28 27 3ad2ant1 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B→A∈V
29 28 ad2antrr ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→A∈V
30 simpll1 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→f:A⟶1-1B
31 f1f ⊢f:A⟶1-1B→f:A⟶B
32 frn ⊢f:A⟶B→ran⁡f⊆B
33 ssralv ⊢ran⁡f⊆B→∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀y∈ran⁡fk⁡y∈g⁡ify∈ran⁡ff-1⁡yx
34 30 31 32 33 4syl ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀y∈ran⁡fk⁡y∈g⁡ify∈ran⁡ff-1⁡yx
35 iftrue ⊢y∈ran⁡f→ify∈ran⁡ff-1⁡yx=f-1⁡y
36 35 fveq2d ⊢y∈ran⁡f→g⁡ify∈ran⁡ff-1⁡yx=g⁡f-1⁡y
37 36 eleq2d ⊢y∈ran⁡f→k⁡y∈g⁡ify∈ran⁡ff-1⁡yx↔k⁡y∈g⁡f-1⁡y
38 37 ralbiia ⊢∀y∈ran⁡fk⁡y∈g⁡ify∈ran⁡ff-1⁡yx↔∀y∈ran⁡fk⁡y∈g⁡f-1⁡y
39 34 38 imbitrdi ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀y∈ran⁡fk⁡y∈g⁡f-1⁡y
40 f1fn ⊢f:A⟶1-1B→fFnA
41 fveq2 ⊢y=f⁡z→k⁡y=k⁡f⁡z
42 2fveq3 ⊢y=f⁡z→g⁡f-1⁡y=g⁡f-1⁡f⁡z
43 41 42 eleq12d ⊢y=f⁡z→k⁡y∈g⁡f-1⁡y↔k⁡f⁡z∈g⁡f-1⁡f⁡z
44 43 ralrn ⊢fFnA→∀y∈ran⁡fk⁡y∈g⁡f-1⁡y↔∀z∈Ak⁡f⁡z∈g⁡f-1⁡f⁡z
45 30 40 44 3syl ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀y∈ran⁡fk⁡y∈g⁡f-1⁡y↔∀z∈Ak⁡f⁡z∈g⁡f-1⁡f⁡z
46 39 45 sylibd ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀z∈Ak⁡f⁡z∈g⁡f-1⁡f⁡z
47 30 7 syl ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→f:A⟶1-1 ontoran⁡f
48 f1ocnvfv1 ⊢f:A⟶1-1 ontoran⁡f∧z∈A→f-1⁡f⁡z=z
49 47 48 sylan ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧z∈A→f-1⁡f⁡z=z
50 49 fveq2d ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧z∈A→g⁡f-1⁡f⁡z=g⁡z
51 50 eleq2d ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧z∈A→k⁡f⁡z∈g⁡f-1⁡f⁡z↔k⁡f⁡z∈g⁡z
52 51 ralbidva ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀z∈Ak⁡f⁡z∈g⁡f-1⁡f⁡z↔∀z∈Ak⁡f⁡z∈g⁡z
53 46 52 sylibd ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X→∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀z∈Ak⁡f⁡z∈g⁡z
54 53 impr ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∀z∈Ak⁡f⁡z∈g⁡z
55 acnlem ⊢A∈V∧∀z∈Ak⁡f⁡z∈g⁡z→∃h∀z∈Ah⁡z∈g⁡z
56 29 54 55 syl2anc ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A∧k:B⟶X∧∀y∈Bk⁡y∈g⁡ify∈ran⁡ff-1⁡yx→∃h∀z∈Ah⁡z∈g⁡z
57 23 56 exlimddv ⊢f:A⟶1-1B∧x∈A∧X∈AC_B∧g∈𝒫X∖∅A→∃h∀z∈Ah⁡z∈g⁡z
58 57 ralrimiva ⊢f:A⟶1-1B∧x∈A∧X∈AC_B→∀g∈𝒫X∖∅A∃h∀z∈Ah⁡z∈g⁡z
59 elex ⊢X∈AC_B→X∈V
60 isacn ⊢X∈V∧A∈V→X∈AC_A↔∀g∈𝒫X∖∅A∃h∀z∈Ah⁡z∈g⁡z
61 59 27 60 syl2anr ⊢f:A⟶1-1B∧X∈AC_B→X∈AC_A↔∀g∈𝒫X∖∅A∃h∀z∈Ah⁡z∈g⁡z
62 61 3adant2 ⊢f:A⟶1-1B∧x∈A∧X∈AC_B→X∈AC_A↔∀g∈𝒫X∖∅A∃h∀z∈Ah⁡z∈g⁡z
63 58 62 mpbird ⊢f:A⟶1-1B∧x∈A∧X∈AC_B→X∈AC_A
64 63 3exp ⊢f:A⟶1-1B→x∈A→X∈AC_B→X∈AC_A
65 64 exlimdv ⊢f:A⟶1-1B→∃xx∈A→X∈AC_B→X∈AC_A
66 2 65 biimtrid ⊢f:A⟶1-1B→¬A=∅→X∈AC_B→X∈AC_A
67 acneq ⊢A=∅→AC_A=AC_∅
68 0fin ⊢∅∈Fin
69 finacn ⊢∅∈Fin→AC_∅=V
70 68 69 ax-mp ⊢AC_∅=V
71 67 70 eqtrdi ⊢A=∅→AC_A=V
72 71 eleq2d ⊢A=∅→X∈AC_A↔X∈V
73 59 72 imbitrrid ⊢A=∅→X∈AC_B→X∈AC_A
74 66 73 pm2.61d2 ⊢f:A⟶1-1B→X∈AC_B→X∈AC_A
75 74 exlimiv ⊢∃ff:A⟶1-1B→X∈AC_B→X∈AC_A
76 1 75 syl ⊢A≼B→X∈AC_B→X∈AC_A