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 f f : A 1-1 B
2 neq0 ¬ A = x x A
3 simpl3 f : A 1-1 B 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-1 B x A X AC _ B g 𝒫 X A y B g : A 𝒫 X
6 simpll1 f : A 1-1 B x A X AC _ B g 𝒫 X A y 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 -1 : ran f 1-1 onto A
9 f1of f -1 : ran f 1-1 onto A f -1 : ran f A
10 6 7 8 9 4syl f : A 1-1 B x A X AC _ B g 𝒫 X A y B f -1 : ran f A
11 10 ffvelrnda f : A 1-1 B x A X AC _ B g 𝒫 X A y B y ran f f -1 y A
12 simpl2 f : A 1-1 B x A X AC _ B g 𝒫 X A x A
13 12 ad2antrr f : A 1-1 B x A X AC _ B g 𝒫 X A y B ¬ y ran f x A
14 11 13 ifclda f : A 1-1 B x A X AC _ B g 𝒫 X A y B if y ran f f -1 y x A
15 5 14 ffvelrnd f : A 1-1 B x A X AC _ B g 𝒫 X A y B g if y ran f f -1 y x 𝒫 X
16 eldifsn g if y ran f f -1 y x 𝒫 X g if y ran f f -1 y x 𝒫 X g if y ran f f -1 y x
17 elpwi g if y ran f f -1 y x 𝒫 X g if y ran f f -1 y x X
18 17 anim1i g if y ran f f -1 y x 𝒫 X g if y ran f f -1 y x g if y ran f f -1 y x X g if y ran f f -1 y x
19 16 18 sylbi g if y ran f f -1 y x 𝒫 X g if y ran f f -1 y x X g if y ran f f -1 y x
20 15 19 syl f : A 1-1 B x A X AC _ B g 𝒫 X A y B g if y ran f f -1 y x X g if y ran f f -1 y x
21 20 ralrimiva f : A 1-1 B x A X AC _ B g 𝒫 X A y B g if y ran f f -1 y x X g if y ran f f -1 y x
22 acni2 X AC _ B y B g if y ran f f -1 y x X g if y ran f f -1 y x k k : B X y B k y g if y ran f f -1 y x
23 3 21 22 syl2anc f : A 1-1 B x A X AC _ B g 𝒫 X A k k : B X y B k y g if y ran f f -1 y x
24 f1dm f : A 1-1 B dom f = A
25 vex f V
26 25 dmex dom f V
27 24 26 eqeltrrdi f : A 1-1 B A V
28 27 3ad2ant1 f : A 1-1 B x A X AC _ B A V
29 28 ad2antrr f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x A V
30 simpll1 f : A 1-1 B x A X AC _ B g 𝒫 X 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 B
33 ssralv ran f B y B k y g if y ran f f -1 y x y ran f k y g if y ran f f -1 y x
34 30 31 32 33 4syl f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x y ran f k y g if y ran f f -1 y x
35 iftrue y ran f if y ran f f -1 y x = f -1 y
36 35 fveq2d y ran f g if y ran f f -1 y x = g f -1 y
37 36 eleq2d y ran f k y g if y ran f f -1 y x k y g f -1 y
38 37 ralbiia y ran f k y g if y ran f f -1 y x y ran f k y g f -1 y
39 34 38 syl6ib f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x y ran f k y g f -1 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 -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 f Fn A y ran f k y g f -1 y z A k f z g f -1 f z
45 30 40 44 3syl f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y ran f k y g f -1 y z A k f z g f -1 f z
46 39 45 sylibd f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x z A k f z g f -1 f z
47 30 7 syl f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X f : A 1-1 onto ran f
48 f1ocnvfv1 f : A 1-1 onto ran f z A f -1 f z = z
49 47 48 sylan f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X z A f -1 f z = z
50 49 fveq2d f : A 1-1 B 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-1 B 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-1 B x A X AC _ B g 𝒫 X A k : B X z A k f z g f -1 f z z A k f z g z
53 46 52 sylibd f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x z A k f z g z
54 53 impr f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x z A k f z g z
55 acnlem A V z A k f z g z h z A h z g z
56 29 54 55 syl2anc f : A 1-1 B x A X AC _ B g 𝒫 X A k : B X y B k y g if y ran f f -1 y x h z A h z g z
57 23 56 exlimddv f : A 1-1 B x A X AC _ B g 𝒫 X A h z A h z g z
58 57 ralrimiva f : A 1-1 B x A X AC _ B g 𝒫 X A h z A h z g z
59 elex X AC _ B X V
60 isacn X V A V X AC _ A g 𝒫 X A h z A h z g z
61 59 27 60 syl2anr f : A 1-1 B X AC _ B X AC _ A g 𝒫 X A h z A h z g z
62 61 3adant2 f : A 1-1 B x A X AC _ B X AC _ A g 𝒫 X A h z A h z g z
63 58 62 mpbird f : A 1-1 B x A X AC _ B X AC _ A
64 63 3exp f : A 1-1 B x A X AC _ B X AC _ A
65 64 exlimdv f : A 1-1 B x x A X AC _ B X AC _ A
66 2 65 syl5bi f : A 1-1 B ¬ 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 syl5ibr A = X AC _ B X AC _ A
74 66 73 pm2.61d2 f : A 1-1 B X AC _ B X AC _ A
75 74 exlimiv f f : A 1-1 B X AC _ B X AC _ A
76 1 75 syl A B X AC _ B X AC _ A