# Metamath Proof Explorer

## Theorem smflimlem2

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem2.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
smflimlem2.2 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smflimlem2.3 ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
smflimlem2.4 ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
smflimlem2.5 ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
smflimlem2.6 ${⊢}{\phi }\to {A}\in ℝ$
smflimlem2.7 ${⊢}{P}=\left({m}\in {Z},{k}\in ℕ⟼\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\right)$
smflimlem2.8 ${⊢}{H}=\left({m}\in {Z},{k}\in ℕ⟼{C}\left({m}{P}{k}\right)\right)$
smflimlem2.9 ${⊢}{I}=\bigcap _{{k}\in ℕ}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
smflimlem2.10 ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}{P}\right)\to {C}\left({r}\right)\in {r}$
Assertion smflimlem2 ${⊢}{\phi }\to \left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {D}\cap {I}$

### Proof

Step Hyp Ref Expression
1 smflimlem2.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 smflimlem2.2 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
3 smflimlem2.3 ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
4 smflimlem2.4 ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
5 smflimlem2.5 ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
6 smflimlem2.6 ${⊢}{\phi }\to {A}\in ℝ$
7 smflimlem2.7 ${⊢}{P}=\left({m}\in {Z},{k}\in ℕ⟼\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\right)$
8 smflimlem2.8 ${⊢}{H}=\left({m}\in {Z},{k}\in ℕ⟼{C}\left({m}{P}{k}\right)\right)$
9 smflimlem2.9 ${⊢}{I}=\bigcap _{{k}\in ℕ}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
10 smflimlem2.10 ${⊢}\left({\phi }\wedge {r}\in \mathrm{ran}{P}\right)\to {C}\left({r}\right)\in {r}$
11 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
12 4 11 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
13 12 ssrab2f ${⊢}\left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {D}$
14 13 a1i ${⊢}{\phi }\to \left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {D}$
15 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to {x}\in {D}$
16 ssrab2 ${⊢}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
17 4 16 eqsstri ${⊢}{D}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
18 17 sseli ${⊢}{x}\in {D}\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
19 fveq2 ${⊢}{n}={i}\to {ℤ}_{\ge {n}}={ℤ}_{\ge {i}}$
20 19 iineq1d ${⊢}{n}={i}\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
21 20 cbviunv ${⊢}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
22 21 eleq2i ${⊢}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)↔{x}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
23 eliun ${⊢}{x}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)↔\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
24 22 23 bitri ${⊢}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)↔\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
25 18 24 sylib ${⊢}{x}\in {D}\to \exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
26 15 25 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to \exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
27 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)$
28 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{k}\in ℕ$
29 27 28 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)$
30 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{i}\in {Z}$
31 29 30 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)$
32 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{x}$
33 nfii1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
34 32 33 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
35 31 34 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)$
36 nfmpt1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)$
37 eqid ${⊢}{ℤ}_{\ge {i}}={ℤ}_{\ge {i}}$
38 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
39 1 eleq2i ${⊢}{i}\in {Z}↔{i}\in {ℤ}_{\ge {M}}$
40 39 biimpi ${⊢}{i}\in {Z}\to {i}\in {ℤ}_{\ge {M}}$
41 38 40 sseldi ${⊢}{i}\in {Z}\to {i}\in ℤ$
42 uzid ${⊢}{i}\in ℤ\to {i}\in {ℤ}_{\ge {i}}$
43 41 42 syl ${⊢}{i}\in {Z}\to {i}\in {ℤ}_{\ge {i}}$
44 43 ad2antlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to {i}\in {ℤ}_{\ge {i}}$
45 simplll ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to \left({\phi }\wedge {x}\in {D}\right)$
46 45 simpld ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {\phi }$
47 uzss ${⊢}{i}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {i}}\subseteq {ℤ}_{\ge {M}}$
48 40 47 syl ${⊢}{i}\in {Z}\to {ℤ}_{\ge {i}}\subseteq {ℤ}_{\ge {M}}$
49 48 1 sseqtrrdi ${⊢}{i}\in {Z}\to {ℤ}_{\ge {i}}\subseteq {Z}$
50 49 sselda ${⊢}\left({i}\in {Z}\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {m}\in {Z}$
51 50 ad4ant24 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {m}\in {Z}$
52 eliinid ${⊢}\left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {x}\in \mathrm{dom}{F}\left({m}\right)$
53 52 adantll ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {x}\in \mathrm{dom}{F}\left({m}\right)$
54 eqidd ${⊢}{\phi }\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)$
55 fvexd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right)\left({x}\right)\in \mathrm{V}$
56 54 55 fvmpt2d ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)={F}\left({m}\right)\left({x}\right)$
57 56 3adant3 ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in \mathrm{dom}{F}\left({m}\right)\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)={F}\left({m}\right)\left({x}\right)$
58 2 adantr ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {S}\in \mathrm{SAlg}$
59 3 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right)\in \mathrm{SMblFn}\left({S}\right)$
60 eqid ${⊢}\mathrm{dom}{F}\left({m}\right)=\mathrm{dom}{F}\left({m}\right)$
61 58 59 60 smff ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
62 61 3adant3 ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in \mathrm{dom}{F}\left({m}\right)\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
63 simp3 ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in \mathrm{dom}{F}\left({m}\right)\right)\to {x}\in \mathrm{dom}{F}\left({m}\right)$
64 62 63 ffvelrnd ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in \mathrm{dom}{F}\left({m}\right)\right)\to {F}\left({m}\right)\left({x}\right)\in ℝ$
65 57 64 eqeltrd ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in \mathrm{dom}{F}\left({m}\right)\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ$
66 46 51 53 65 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ$
67 66 adantl3r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ$
68 67 adantl3r ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ$
69 4 eleq2i ${⊢}{x}\in {D}↔{x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
70 69 biimpi ${⊢}{x}\in {D}\to {x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
71 rabidim2 ${⊢}{x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
72 70 71 syl ${⊢}{x}\in {D}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
73 climdm ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
74 72 73 sylib ${⊢}{x}\in {D}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
75 74 adantl ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
76 75 73 sylibr ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
77 76 73 sylib ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
78 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
79 simpr ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {x}\in {D}$
80 12 78 5 79 fnlimfv ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {G}\left({x}\right)=⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
81 80 eqcomd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to ⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)={G}\left({x}\right)$
82 77 81 breqtrd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝{G}\left({x}\right)$
83 82 ad4antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)⇝{G}\left({x}\right)$
84 6 ad5antr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to {A}\in ℝ$
85 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to {G}\left({x}\right)\le {A}$
86 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to {k}\in ℕ$
87 nnrecrp ${⊢}{k}\in ℕ\to \frac{1}{{k}}\in {ℝ}^{+}$
88 86 87 syl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \frac{1}{{k}}\in {ℝ}^{+}$
89 35 36 37 44 68 83 84 85 88 climleltrp ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)$
90 simp-6l ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to {\phi }$
91 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to {i}\in {Z}$
92 91 adantr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to {i}\in {Z}$
93 simplr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
94 simpr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to {n}\in {ℤ}_{\ge {i}}$
95 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
96 95 30 34 nf3an ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)$
97 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{n}\in {ℤ}_{\ge {i}}$
98 96 97 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)$
99 simpll ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)$
100 37 uztrn2 ${⊢}\left({n}\in {ℤ}_{\ge {i}}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {ℤ}_{\ge {i}}$
101 100 adantll ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {ℤ}_{\ge {i}}$
102 simpll2 ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {i}\in {Z}$
103 simplr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {m}\in {ℤ}_{\ge {i}}$
104 102 103 50 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {m}\in {Z}$
105 simpr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)$
106 id ${⊢}{m}\in {Z}\to {m}\in {Z}$
107 fvexd ${⊢}{m}\in {Z}\to {F}\left({m}\right)\left({x}\right)\in \mathrm{V}$
108 eqid ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)$
109 108 fvmpt2 ${⊢}\left({m}\in {Z}\wedge {F}\left({m}\right)\left({x}\right)\in \mathrm{V}\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)={F}\left({m}\right)\left({x}\right)$
110 106 107 109 syl2anc ${⊢}{m}\in {Z}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)={F}\left({m}\right)\left({x}\right)$
111 110 eqcomd ${⊢}{m}\in {Z}\to {F}\left({m}\right)\left({x}\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)$
112 111 adantr ${⊢}\left({m}\in {Z}\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {F}\left({m}\right)\left({x}\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)$
113 simpr ${⊢}\left({m}\in {Z}\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)$
114 112 113 eqbrtrd ${⊢}\left({m}\in {Z}\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)$
115 104 105 114 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)$
116 52 3ad2antl3 ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to {x}\in \mathrm{dom}{F}\left({m}\right)$
117 116 adantr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {x}\in \mathrm{dom}{F}\left({m}\right)$
118 simpr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)$
119 117 118 jca ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \left({x}\in \mathrm{dom}{F}\left({m}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)$
120 rabid ${⊢}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}↔\left({x}\in \mathrm{dom}{F}\left({m}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)$
121 119 120 sylibr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge {F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
122 115 121 syldan ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
123 122 adantrl ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\wedge \left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
124 123 ex ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {m}\in {ℤ}_{\ge {i}}\right)\to \left(\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
125 99 101 124 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left(\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
126 98 125 ralimdaa ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
127 90 92 93 94 126 syl31anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\wedge {n}\in {ℤ}_{\ge {i}}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
128 127 reximdva ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \left(\exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)\in ℝ\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\left({m}\right)<{A}+\left(\frac{1}{{k}}\right)\right)\to \exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
129 89 128 mpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
130 ssrexv ${⊢}{ℤ}_{\ge {i}}\subseteq {Z}\to \left(\exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
131 49 130 syl ${⊢}{i}\in {Z}\to \left(\exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
132 131 ad2antlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \left(\exists {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
133 129 132 mpd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {i}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
134 133 rexlimdva2 ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to \left(\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
135 26 134 mpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
136 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)$
137 nfra1 ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
138 136 137 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)$
139 simpll1 ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {\phi }$
140 simpll2 ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {k}\in ℕ$
141 1 uztrn2 ${⊢}\left({n}\in {Z}\wedge {j}\in {ℤ}_{\ge {n}}\right)\to {j}\in {Z}$
142 141 ssd ${⊢}{n}\in {Z}\to {ℤ}_{\ge {n}}\subseteq {Z}$
143 142 sselda ${⊢}\left({n}\in {Z}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
144 143 adantll ${⊢}\left(\left({k}\in ℕ\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
145 144 3adantl1 ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
146 145 adantlr ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
147 rspa ${⊢}\left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
148 147 adantll ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
149 simp1 ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {\phi }$
150 simp3 ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {m}\in {Z}$
151 simp2 ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {k}\in ℕ$
152 eqid ${⊢}\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}=\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
153 152 2 rabexd ${⊢}{\phi }\to \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}$
154 153 ralrimivw ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}$
155 154 ralrimivw ${⊢}{\phi }\to \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}$
156 155 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}$
157 7 elrnmpoid ${⊢}\left({m}\in {Z}\wedge {k}\in ℕ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}\right)\to {m}{P}{k}\in \mathrm{ran}{P}$
158 150 151 156 157 syl3anc ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {m}{P}{k}\in \mathrm{ran}{P}$
159 ovex ${⊢}{m}{P}{k}\in \mathrm{V}$
160 eleq1 ${⊢}{r}={m}{P}{k}\to \left({r}\in \mathrm{ran}{P}↔{m}{P}{k}\in \mathrm{ran}{P}\right)$
161 160 anbi2d ${⊢}{r}={m}{P}{k}\to \left(\left({\phi }\wedge {r}\in \mathrm{ran}{P}\right)↔\left({\phi }\wedge {m}{P}{k}\in \mathrm{ran}{P}\right)\right)$
162 fveq2 ${⊢}{r}={m}{P}{k}\to {C}\left({r}\right)={C}\left({m}{P}{k}\right)$
163 id ${⊢}{r}={m}{P}{k}\to {r}={m}{P}{k}$
164 162 163 eleq12d ${⊢}{r}={m}{P}{k}\to \left({C}\left({r}\right)\in {r}↔{C}\left({m}{P}{k}\right)\in \left({m}{P}{k}\right)\right)$
165 161 164 imbi12d ${⊢}{r}={m}{P}{k}\to \left(\left(\left({\phi }\wedge {r}\in \mathrm{ran}{P}\right)\to {C}\left({r}\right)\in {r}\right)↔\left(\left({\phi }\wedge {m}{P}{k}\in \mathrm{ran}{P}\right)\to {C}\left({m}{P}{k}\right)\in \left({m}{P}{k}\right)\right)\right)$
166 159 165 10 vtocl ${⊢}\left({\phi }\wedge {m}{P}{k}\in \mathrm{ran}{P}\right)\to {C}\left({m}{P}{k}\right)\in \left({m}{P}{k}\right)$
167 149 158 166 syl2anc ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {C}\left({m}{P}{k}\right)\in \left({m}{P}{k}\right)$
168 fvexd ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {C}\left({m}{P}{k}\right)\in \mathrm{V}$
169 8 ovmpt4g ${⊢}\left({m}\in {Z}\wedge {k}\in ℕ\wedge {C}\left({m}{P}{k}\right)\in \mathrm{V}\right)\to {m}{H}{k}={C}\left({m}{P}{k}\right)$
170 150 151 168 169 syl3anc ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {m}{H}{k}={C}\left({m}{P}{k}\right)$
171 170 eqcomd ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {C}\left({m}{P}{k}\right)={m}{H}{k}$
172 149 153 syl ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}$
173 7 ovmpt4g ${⊢}\left({m}\in {Z}\wedge {k}\in ℕ\wedge \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\in \mathrm{V}\right)\to {m}{P}{k}=\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
174 150 151 172 173 syl3anc ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {m}{P}{k}=\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
175 171 174 eleq12d ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \left({C}\left({m}{P}{k}\right)\in \left({m}{P}{k}\right)↔{m}{H}{k}\in \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}\right)$
176 167 175 mpbid ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to {m}{H}{k}\in \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
177 ineq1 ${⊢}{s}={m}{H}{k}\to {s}\cap \mathrm{dom}{F}\left({m}\right)=\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)$
178 177 eqeq2d ${⊢}{s}={m}{H}{k}\to \left(\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)↔\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}=\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)\right)$
179 178 elrab ${⊢}{m}{H}{k}\in \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}↔\left({m}{H}{k}\in {S}\wedge \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}=\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)\right)$
180 176 179 sylib ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \left({m}{H}{k}\in {S}\wedge \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}=\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)\right)$
181 180 simprd ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}=\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)$
182 inss1 ${⊢}\left({m}{H}{k}\right)\cap \mathrm{dom}{F}\left({m}\right)\subseteq {m}{H}{k}$
183 181 182 eqsstrdi ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\to \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\subseteq {m}{H}{k}$
184 183 adantr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\wedge {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\subseteq {m}{H}{k}$
185 simpr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\wedge {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}$
186 184 185 sseldd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {m}\in {Z}\right)\wedge {x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to {x}\in \left({m}{H}{k}\right)$
187 139 140 146 148 186 syl31anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in \left({m}{H}{k}\right)$
188 187 ex ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to \left({m}\in {ℤ}_{\ge {n}}\to {x}\in \left({m}{H}{k}\right)\right)$
189 138 188 ralrimi ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left({m}{H}{k}\right)$
190 vex ${⊢}{x}\in \mathrm{V}$
191 eliin ${⊢}{x}\in \mathrm{V}\to \left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)↔\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left({m}{H}{k}\right)\right)$
192 190 191 ax-mp ${⊢}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)↔\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left({m}{H}{k}\right)$
193 189 192 sylibr ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\wedge \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\right)\to {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
194 193 ex ${⊢}\left({\phi }\wedge {k}\in ℕ\wedge {n}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)\right)$
195 194 ad5ant145 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\wedge {n}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)\right)$
196 195 reximdva ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{A}+\left(\frac{1}{{k}}\right)\right\}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)\right)$
197 135 196 mpd ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
198 eliun ${⊢}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
199 197 198 sylibr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\wedge {k}\in ℕ\right)\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
200 199 ralrimiva ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
201 eliin ${⊢}{x}\in \mathrm{V}\to \left({x}\in \bigcap _{{k}\in ℕ}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)\right)$
202 190 201 ax-mp ${⊢}{x}\in \bigcap _{{k}\in ℕ}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
203 200 202 sylibr ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\to {x}\in \bigcap _{{k}\in ℕ}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\left({m}{H}{k}\right)$
204 203 9 eleqtrrdi ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {G}\left({x}\right)\le {A}\right)\to {x}\in {I}$
205 204 ex ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({G}\left({x}\right)\le {A}\to {x}\in {I}\right)$
206 205 ralrimiva ${⊢}{\phi }\to \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)\le {A}\to {x}\in {I}\right)$
207 rabss ${⊢}\left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {I}↔\forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)\le {A}\to {x}\in {I}\right)$
208 206 207 sylibr ${⊢}{\phi }\to \left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {I}$
209 14 208 ssind ${⊢}{\phi }\to \left\{{x}\in {D}|{G}\left({x}\right)\le {A}\right\}\subseteq {D}\cap {I}$