Metamath Proof Explorer

Theorem axdc4uzlem

Description: Lemma for axdc4uz . (Contributed by Mario Carneiro, 8-Jan-2014) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses axdc4uz.1 ⊢M∈ℤ
axdc4uz.2 ⊢Z=ℤ≥M
axdc4uz.3 ⊢A∈V
axdc4uz.4 ⊢G=rec⁡y∈V⟼y+1M↾ω
axdc4uz.5 ⊢H=n∈ω,x∈A⟼G⁡nFx
Assertion axdc4uzlem ⊢C∈A∧F:Z×A⟶𝒫A∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k

Proof

Step Hyp Ref Expression
1 axdc4uz.1 ⊢M∈ℤ
2 axdc4uz.2 ⊢Z=ℤ≥M
3 axdc4uz.3 ⊢A∈V
4 axdc4uz.4 ⊢G=rec⁡y∈V⟼y+1M↾ω
5 axdc4uz.5 ⊢H=n∈ω,x∈A⟼G⁡nFx
6 1 4 om2uzf1oi ⊢G:ω⟶1-1 ontoℤ≥M
7 f1oeq3 ⊢Z=ℤ≥M→G:ω⟶1-1 ontoZ↔G:ω⟶1-1 ontoℤ≥M
8 2 7 ax-mp ⊢G:ω⟶1-1 ontoZ↔G:ω⟶1-1 ontoℤ≥M
9 6 8 mpbir ⊢G:ω⟶1-1 ontoZ
10 f1of ⊢G:ω⟶1-1 ontoZ→G:ω⟶Z
11 9 10 ax-mp ⊢G:ω⟶Z
12 11 ffvelcdmi ⊢n∈ω→G⁡n∈Z
13 fovcdm ⊢F:Z×A⟶𝒫A∖∅∧G⁡n∈Z∧x∈A→G⁡nFx∈𝒫A∖∅
14 12 13 syl3an2 ⊢F:Z×A⟶𝒫A∖∅∧n∈ω∧x∈A→G⁡nFx∈𝒫A∖∅
15 14 3expb ⊢F:Z×A⟶𝒫A∖∅∧n∈ω∧x∈A→G⁡nFx∈𝒫A∖∅
16 15 ralrimivva ⊢F:Z×A⟶𝒫A∖∅→∀n∈ω∀x∈AG⁡nFx∈𝒫A∖∅
17 5 fmpo ⊢∀n∈ω∀x∈AG⁡nFx∈𝒫A∖∅↔H:ω×A⟶𝒫A∖∅
18 16 17 sylib ⊢F:Z×A⟶𝒫A∖∅→H:ω×A⟶𝒫A∖∅
19 3 axdc4 ⊢C∈A∧H:ω×A⟶𝒫A∖∅→∃ff:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m
20 18 19 sylan2 ⊢C∈A∧F:Z×A⟶𝒫A∖∅→∃ff:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m
21 f1ocnv ⊢G:ω⟶1-1 ontoZ→G-1:Z⟶1-1 ontoω
22 f1of ⊢G-1:Z⟶1-1 ontoω→G-1:Z⟶ω
23 9 21 22 mp2b ⊢G-1:Z⟶ω
24 fco ⊢f:ω⟶A∧G-1:Z⟶ω→f∘G-1:Z⟶A
25 23 24 mpan2 ⊢f:ω⟶A→f∘G-1:Z⟶A
26 25 3ad2ant1 ⊢f:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→f∘G-1:Z⟶A
27 uzid ⊢M∈ℤ→M∈ℤ≥M
28 1 27 ax-mp ⊢M∈ℤ≥M
29 28 2 eleqtrri ⊢M∈Z
30 fvco3 ⊢G-1:Z⟶ω∧M∈Z→f∘G-1⁡M=f⁡G-1⁡M
31 23 29 30 mp2an ⊢f∘G-1⁡M=f⁡G-1⁡M
32 1 4 om2uz0i ⊢G⁡∅=M
33 peano1 ⊢∅∈ω
34 f1ocnvfv ⊢G:ω⟶1-1 ontoZ∧∅∈ω→G⁡∅=M→G-1⁡M=∅
35 9 33 34 mp2an ⊢G⁡∅=M→G-1⁡M=∅
36 32 35 ax-mp ⊢G-1⁡M=∅
37 36 fveq2i ⊢f⁡G-1⁡M=f⁡∅
38 31 37 eqtri ⊢f∘G-1⁡M=f⁡∅
39 simp2 ⊢f:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→f⁡∅=C
40 38 39 eqtrid ⊢f:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→f∘G-1⁡M=C
41 23 ffvelcdmi ⊢k∈Z→G-1⁡k∈ω
42 41 adantl ⊢f:ω⟶A∧k∈Z→G-1⁡k∈ω
43 suceq ⊢m=G-1⁡k→suc⁡m=suc⁡G-1⁡k
44 43 fveq2d ⊢m=G-1⁡k→f⁡suc⁡m=f⁡suc⁡G-1⁡k
45 id ⊢m=G-1⁡k→m=G-1⁡k
46 fveq2 ⊢m=G-1⁡k→f⁡m=f⁡G-1⁡k
47 45 46 oveq12d ⊢m=G-1⁡k→mHf⁡m=G-1⁡kHf⁡G-1⁡k
48 44 47 eleq12d ⊢m=G-1⁡k→f⁡suc⁡m∈mHf⁡m↔f⁡suc⁡G-1⁡k∈G-1⁡kHf⁡G-1⁡k
49 48 rspcv ⊢G-1⁡k∈ω→∀m∈ωf⁡suc⁡m∈mHf⁡m→f⁡suc⁡G-1⁡k∈G-1⁡kHf⁡G-1⁡k
50 42 49 syl ⊢f:ω⟶A∧k∈Z→∀m∈ωf⁡suc⁡m∈mHf⁡m→f⁡suc⁡G-1⁡k∈G-1⁡kHf⁡G-1⁡k
51 2 peano2uzs ⊢k∈Z→k+1∈Z
52 fvco3 ⊢G-1:Z⟶ω∧k+1∈Z→f∘G-1⁡k+1=f⁡G-1⁡k+1
53 23 51 52 sylancr ⊢k∈Z→f∘G-1⁡k+1=f⁡G-1⁡k+1
54 1 4 om2uzsuci ⊢G-1⁡k∈ω→G⁡suc⁡G-1⁡k=G⁡G-1⁡k+1
55 41 54 syl ⊢k∈Z→G⁡suc⁡G-1⁡k=G⁡G-1⁡k+1
56 f1ocnvfv2 ⊢G:ω⟶1-1 ontoZ∧k∈Z→G⁡G-1⁡k=k
57 9 56 mpan ⊢k∈Z→G⁡G-1⁡k=k
58 57 oveq1d ⊢k∈Z→G⁡G-1⁡k+1=k+1
59 55 58 eqtrd ⊢k∈Z→G⁡suc⁡G-1⁡k=k+1
60 peano2 ⊢G-1⁡k∈ω→suc⁡G-1⁡k∈ω
61 41 60 syl ⊢k∈Z→suc⁡G-1⁡k∈ω
62 f1ocnvfv ⊢G:ω⟶1-1 ontoZ∧suc⁡G-1⁡k∈ω→G⁡suc⁡G-1⁡k=k+1→G-1⁡k+1=suc⁡G-1⁡k
63 9 61 62 sylancr ⊢k∈Z→G⁡suc⁡G-1⁡k=k+1→G-1⁡k+1=suc⁡G-1⁡k
64 59 63 mpd ⊢k∈Z→G-1⁡k+1=suc⁡G-1⁡k
65 64 fveq2d ⊢k∈Z→f⁡G-1⁡k+1=f⁡suc⁡G-1⁡k
66 53 65 eqtr2d ⊢k∈Z→f⁡suc⁡G-1⁡k=f∘G-1⁡k+1
67 66 adantl ⊢f:ω⟶A∧k∈Z→f⁡suc⁡G-1⁡k=f∘G-1⁡k+1
68 ffvelcdm ⊢f:ω⟶A∧G-1⁡k∈ω→f⁡G-1⁡k∈A
69 41 68 sylan2 ⊢f:ω⟶A∧k∈Z→f⁡G-1⁡k∈A
70 fveq2 ⊢n=G-1⁡k→G⁡n=G⁡G-1⁡k
71 70 oveq1d ⊢n=G-1⁡k→G⁡nFx=G⁡G-1⁡kFx
72 oveq2 ⊢x=f⁡G-1⁡k→G⁡G-1⁡kFx=G⁡G-1⁡kFf⁡G-1⁡k
73 ovex ⊢G⁡G-1⁡kFf⁡G-1⁡k∈V
74 71 72 5 73 ovmpo ⊢G-1⁡k∈ω∧f⁡G-1⁡k∈A→G-1⁡kHf⁡G-1⁡k=G⁡G-1⁡kFf⁡G-1⁡k
75 42 69 74 syl2anc ⊢f:ω⟶A∧k∈Z→G-1⁡kHf⁡G-1⁡k=G⁡G-1⁡kFf⁡G-1⁡k
76 fvco3 ⊢G-1:Z⟶ω∧k∈Z→f∘G-1⁡k=f⁡G-1⁡k
77 23 76 mpan ⊢k∈Z→f∘G-1⁡k=f⁡G-1⁡k
78 77 eqcomd ⊢k∈Z→f⁡G-1⁡k=f∘G-1⁡k
79 57 78 oveq12d ⊢k∈Z→G⁡G-1⁡kFf⁡G-1⁡k=kFf∘G-1⁡k
80 79 adantl ⊢f:ω⟶A∧k∈Z→G⁡G-1⁡kFf⁡G-1⁡k=kFf∘G-1⁡k
81 75 80 eqtrd ⊢f:ω⟶A∧k∈Z→G-1⁡kHf⁡G-1⁡k=kFf∘G-1⁡k
82 67 81 eleq12d ⊢f:ω⟶A∧k∈Z→f⁡suc⁡G-1⁡k∈G-1⁡kHf⁡G-1⁡k↔f∘G-1⁡k+1∈kFf∘G-1⁡k
83 50 82 sylibd ⊢f:ω⟶A∧k∈Z→∀m∈ωf⁡suc⁡m∈mHf⁡m→f∘G-1⁡k+1∈kFf∘G-1⁡k
84 83 impancom ⊢f:ω⟶A∧∀m∈ωf⁡suc⁡m∈mHf⁡m→k∈Z→f∘G-1⁡k+1∈kFf∘G-1⁡k
85 84 ralrimiv ⊢f:ω⟶A∧∀m∈ωf⁡suc⁡m∈mHf⁡m→∀k∈Zf∘G-1⁡k+1∈kFf∘G-1⁡k
86 85 3adant2 ⊢f:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→∀k∈Zf∘G-1⁡k+1∈kFf∘G-1⁡k
87 vex ⊢f∈V
88 rdgfun ⊢Fun⁡rec⁡y∈V⟼y+1M
89 omex ⊢ω∈V
90 resfunexg ⊢Fun⁡rec⁡y∈V⟼y+1M∧ω∈V→rec⁡y∈V⟼y+1M↾ω∈V
91 88 89 90 mp2an ⊢rec⁡y∈V⟼y+1M↾ω∈V
92 4 91 eqeltri ⊢G∈V
93 92 cnvex ⊢G-1∈V
94 87 93 coex ⊢f∘G-1∈V
95 feq1 ⊢g=f∘G-1→g:Z⟶A↔f∘G-1:Z⟶A
96 fveq1 ⊢g=f∘G-1→g⁡M=f∘G-1⁡M
97 96 eqeq1d ⊢g=f∘G-1→g⁡M=C↔f∘G-1⁡M=C
98 fveq1 ⊢g=f∘G-1→g⁡k+1=f∘G-1⁡k+1
99 fveq1 ⊢g=f∘G-1→g⁡k=f∘G-1⁡k
100 99 oveq2d ⊢g=f∘G-1→kFg⁡k=kFf∘G-1⁡k
101 98 100 eleq12d ⊢g=f∘G-1→g⁡k+1∈kFg⁡k↔f∘G-1⁡k+1∈kFf∘G-1⁡k
102 101 ralbidv ⊢g=f∘G-1→∀k∈Zg⁡k+1∈kFg⁡k↔∀k∈Zf∘G-1⁡k+1∈kFf∘G-1⁡k
103 95 97 102 3anbi123d ⊢g=f∘G-1→g:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k↔f∘G-1:Z⟶A∧f∘G-1⁡M=C∧∀k∈Zf∘G-1⁡k+1∈kFf∘G-1⁡k
104 94 103 spcev ⊢f∘G-1:Z⟶A∧f∘G-1⁡M=C∧∀k∈Zf∘G-1⁡k+1∈kFf∘G-1⁡k→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
105 26 40 86 104 syl3anc ⊢f:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
106 105 exlimiv ⊢∃ff:ω⟶A∧f⁡∅=C∧∀m∈ωf⁡suc⁡m∈mHf⁡m→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
107 20 106 syl ⊢C∈A∧F:Z×A⟶𝒫A∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k