# Metamath Proof Explorer

## Theorem smflim

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflim.n ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}$
smflim.x ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
smflim.m ${⊢}{\phi }\to {M}\in ℤ$
smflim.z ${⊢}{Z}={ℤ}_{\ge {M}}$
smflim.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smflim.f ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
smflim.d ${⊢}{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\}$
smflim.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
Assertion smflim ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 smflim.n ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}$
2 smflim.x ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
3 smflim.m ${⊢}{\phi }\to {M}\in ℤ$
4 smflim.z ${⊢}{Z}={ℤ}_{\ge {M}}$
5 smflim.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
6 smflim.f ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
7 smflim.d ${⊢}{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\}$
8 smflim.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)$
9 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}{\phi }$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Z}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge {n}}$
12 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{m}$
13 2 12 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)$
14 13 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)$
15 11 14 nfiin ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
16 10 15 nfiun ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
17 16 ssrab2f ${⊢}\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)$
18 7 17 eqsstri ${⊢}{D}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
19 18 a1i ${⊢}{\phi }\to {D}\subseteq \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
20 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
21 4 eleq2i ${⊢}{n}\in {Z}↔{n}\in {ℤ}_{\ge {M}}$
22 21 biimpi ${⊢}{n}\in {Z}\to {n}\in {ℤ}_{\ge {M}}$
23 20 22 sseldi ${⊢}{n}\in {Z}\to {n}\in ℤ$
24 uzid ${⊢}{n}\in ℤ\to {n}\in {ℤ}_{\ge {n}}$
25 23 24 syl ${⊢}{n}\in {Z}\to {n}\in {ℤ}_{\ge {n}}$
26 25 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {n}\in {ℤ}_{\ge {n}}$
27 5 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {S}\in \mathrm{SAlg}$
28 6 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\in \mathrm{SMblFn}\left({S}\right)$
29 eqid ${⊢}\mathrm{dom}{F}\left({n}\right)=\mathrm{dom}{F}\left({n}\right)$
30 27 28 29 smfdmss ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{dom}{F}\left({n}\right)\subseteq \bigcup {S}$
31 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{n}$
32 1 31 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)$
33 32 nfdm ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({n}\right)$
34 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcup {S}$
35 33 34 nfss ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({n}\right)\subseteq \bigcup {S}$
36 fveq2 ${⊢}{m}={n}\to {F}\left({m}\right)={F}\left({n}\right)$
37 36 dmeqd ${⊢}{m}={n}\to \mathrm{dom}{F}\left({m}\right)=\mathrm{dom}{F}\left({n}\right)$
38 37 sseq1d ${⊢}{m}={n}\to \left(\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}↔\mathrm{dom}{F}\left({n}\right)\subseteq \bigcup {S}\right)$
39 35 38 rspce ${⊢}\left({n}\in {ℤ}_{\ge {n}}\wedge \mathrm{dom}{F}\left({n}\right)\subseteq \bigcup {S}\right)\to \exists {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}$
40 26 30 39 syl2anc ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \exists {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}$
41 iinss ${⊢}\exists {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}$
42 40 41 syl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}$
43 42 iunssd ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)\subseteq \bigcup {S}$
44 19 43 sstrd ${⊢}{\phi }\to {D}\subseteq \bigcup {S}$
45 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
46 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{y}$
47 nfmpt1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)$
48 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\mathrm{dom}⇝$
49 47 48 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
50 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{Z}$
51 nfii1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
52 50 51 nfiun ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
53 49 52 nfrab ${⊢}\underset{_}{Ⅎ}{m}\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\}$
54 7 53 nfcxfr ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{D}$
55 46 54 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{y}\in {D}$
56 45 55 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {y}\in {D}\right)$
57 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{F}$
58 5 adantr ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {S}\in \mathrm{SAlg}$
59 6 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 adantlr ${⊢}\left(\left({\phi }\wedge {y}\in {D}\right)\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
63 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
64 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
65 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
66 13 65 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({y}\right)$
67 10 66 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)$
68 67 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝$
69 fveq2 ${⊢}{x}={y}\to {F}\left({m}\right)\left({x}\right)={F}\left({m}\right)\left({y}\right)$
70 69 mpteq2dv ${⊢}{x}={y}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)$
71 70 eleq1d ${⊢}{x}={y}\to \left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right)$
72 16 63 64 68 71 cbvrab ${⊢}\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\}=\left\{{y}\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({y}\right)\right)\in \mathrm{dom}⇝\right\}$
73 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({m}\right)$
74 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{l}$
75 1 74 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)$
76 75 nfdm ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({l}\right)$
77 fveq2 ${⊢}{m}={l}\to {F}\left({m}\right)={F}\left({l}\right)$
78 77 dmeqd ${⊢}{m}={l}\to \mathrm{dom}{F}\left({m}\right)=\mathrm{dom}{F}\left({l}\right)$
79 73 76 78 cbviin ${⊢}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcap _{{l}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({l}\right)$
80 79 a1i ${⊢}{n}={i}\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcap _{{l}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({l}\right)$
81 fveq2 ${⊢}{n}={i}\to {ℤ}_{\ge {n}}={ℤ}_{\ge {i}}$
82 eqidd ${⊢}\left({n}={i}\wedge {l}\in {ℤ}_{\ge {i}}\right)\to \mathrm{dom}{F}\left({l}\right)=\mathrm{dom}{F}\left({l}\right)$
83 81 82 iineq12dv ${⊢}{n}={i}\to \bigcap _{{l}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({l}\right)=\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)$
84 80 83 eqtrd ${⊢}{n}={i}\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)$
85 84 cbviunv ${⊢}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)$
86 85 eleq2i ${⊢}{y}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)↔{y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)$
87 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}{Z}$
88 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({y}\right)$
89 75 46 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({y}\right)$
90 77 fveq1d ${⊢}{m}={l}\to {F}\left({m}\right)\left({y}\right)={F}\left({l}\right)\left({y}\right)$
91 50 87 88 89 90 cbvmptf ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)$
92 91 eleq1i ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝↔\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝$
93 86 92 anbi12i ${⊢}\left({y}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right)↔\left({y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)\wedge \left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right)$
94 93 rabbia2 ${⊢}\left\{{y}\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({y}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}$
95 7 72 94 3eqtri ${⊢}{D}=\left\{{y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}$
96 fveq2 ${⊢}{y}={w}\to {F}\left({l}\right)\left({y}\right)={F}\left({l}\right)\left({w}\right)$
97 96 mpteq2dv ${⊢}{y}={w}\to \left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)$
98 97 eleq1d ${⊢}{y}={w}\to \left(\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝↔\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right)$
99 98 cbvrabv ${⊢}\left\{{y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right\}$
100 fveq2 ${⊢}{l}={m}\to {F}\left({l}\right)={F}\left({m}\right)$
101 100 dmeqd ${⊢}{l}={m}\to \mathrm{dom}{F}\left({l}\right)=\mathrm{dom}{F}\left({m}\right)$
102 76 73 101 cbviin ${⊢}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)=\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
103 102 a1i ${⊢}{i}\in {Z}\to \bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)=\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
104 103 iuneq2i ${⊢}\bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)=\bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
105 104 eleq2i ${⊢}{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)↔{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)$
106 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{w}$
107 75 106 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({w}\right)$
108 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({w}\right)$
109 100 fveq1d ${⊢}{l}={m}\to {F}\left({l}\right)\left({w}\right)={F}\left({m}\right)\left({w}\right)$
110 87 50 107 108 109 cbvmptf ${⊢}\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)=\left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)$
111 110 eleq1i ${⊢}\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)\in \mathrm{dom}⇝$
112 105 111 anbi12i ${⊢}\left({w}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)\wedge \left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right)↔\left({w}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)\wedge \left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right)$
113 112 rabbia2 ${⊢}\left\{{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right\}$
114 99 113 eqtri ${⊢}\left\{{y}\in \bigcup _{{i}\in {Z}}\bigcap _{{l}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({l}\right)|\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right\}$
115 95 114 eqtri ${⊢}{D}=\left\{{w}\in \bigcup _{{i}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {i}}}\mathrm{dom}{F}\left({m}\right)|\left({m}\in {Z}⟼{F}\left({m}\right)\left({w}\right)\right)\in \mathrm{dom}⇝\right\}$
116 simpr ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to {y}\in {D}$
117 56 1 57 4 62 115 116 fnlimfvre ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to ⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\right)\in ℝ$
118 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\}$
119 7 118 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
120 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{D}$
121 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)$
122 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⇝$
123 122 67 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\right)$
124 70 fveq2d ${⊢}{x}={y}\to ⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\right)$
125 119 120 121 123 124 cbvmptf ${⊢}\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)=\left({y}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\right)\right)$
126 8 125 eqtri ${⊢}{G}=\left({y}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({y}\right)\right)\right)\right)$
127 117 126 fmptd ${⊢}{\phi }\to {G}:{D}⟶ℝ$
128 3 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {M}\in ℤ$
129 5 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {S}\in \mathrm{SAlg}$
130 6 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
131 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{l}$
132 2 131 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)$
133 132 65 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({y}\right)$
134 10 133 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)$
135 122 134 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⇝\left(\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\right)$
136 nfcv ${⊢}\underset{_}{Ⅎ}{l}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({x}\right)$
137 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{x}$
138 75 137 nffv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({x}\right)$
139 77 fveq1d ${⊢}{m}={l}\to {F}\left({m}\right)\left({x}\right)={F}\left({l}\right)\left({x}\right)$
140 50 87 136 138 139 cbvmptf ${⊢}\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({x}\right)\right)$
141 140 a1i ${⊢}{x}={y}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({x}\right)\right)$
142 simpl ${⊢}\left({x}={y}\wedge {l}\in {Z}\right)\to {x}={y}$
143 142 fveq2d ${⊢}\left({x}={y}\wedge {l}\in {Z}\right)\to {F}\left({l}\right)\left({x}\right)={F}\left({l}\right)\left({y}\right)$
144 143 mpteq2dva ${⊢}{x}={y}\to \left({l}\in {Z}⟼{F}\left({l}\right)\left({x}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)$
145 141 144 eqtrd ${⊢}{x}={y}\to \left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)=\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)$
146 145 fveq2d ${⊢}{x}={y}\to ⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)=⇝\left(\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\right)$
147 119 120 121 135 146 cbvmptf ${⊢}\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{F}\left({m}\right)\left({x}\right)\right)\right)\right)=\left({y}\in {D}⟼⇝\left(\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\right)\right)$
148 8 147 eqtri ${⊢}{G}=\left({y}\in {D}⟼⇝\left(\left({l}\in {Z}⟼{F}\left({l}\right)\left({y}\right)\right)\right)\right)$
149 simpr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {a}\in ℝ$
150 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}<$
151 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({a}+\left(\frac{1}{{j}}\right)\right)$
152 89 150 151 nfbr ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)$
153 152 76 nfrab ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}$
154 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{t}$
155 154 76 nfin ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({t}\cap \mathrm{dom}{F}\left({l}\right)\right)$
156 153 155 nfeq ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)$
157 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{S}$
158 156 157 nfrab ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}$
159 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}$
160 nfcv ${⊢}\underset{_}{Ⅎ}{l}\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\}$
161 nfcv ${⊢}\underset{_}{Ⅎ}{j}\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\}$
162 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({l}\right)$
163 132 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({l}\right)$
164 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}<$
165 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({a}+\left(\frac{1}{{j}}\right)\right)$
166 133 164 165 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)$
167 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)$
168 fveq2 ${⊢}{y}={x}\to {F}\left({l}\right)\left({y}\right)={F}\left({l}\right)\left({x}\right)$
169 168 breq1d ${⊢}{y}={x}\to \left({F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)↔{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right)$
170 162 163 166 167 169 cbvrab ${⊢}\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}=\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}$
171 170 a1i ${⊢}{t}={s}\to \left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}=\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}$
172 ineq1 ${⊢}{t}={s}\to {t}\cap \mathrm{dom}{F}\left({l}\right)={s}\cap \mathrm{dom}{F}\left({l}\right)$
173 171 172 eqeq12d ${⊢}{t}={s}\to \left(\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)↔\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({l}\right)\right)$
174 173 cbvrabv ${⊢}\left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}=\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({l}\right)\right\}$
175 174 a1i ${⊢}{l}={m}\to \left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}=\left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({l}\right)\right\}$
176 101 eleq2d ${⊢}{l}={m}\to \left({x}\in \mathrm{dom}{F}\left({l}\right)↔{x}\in \mathrm{dom}{F}\left({m}\right)\right)$
177 100 fveq1d ${⊢}{l}={m}\to {F}\left({l}\right)\left({x}\right)={F}\left({m}\right)\left({x}\right)$
178 177 breq1d ${⊢}{l}={m}\to \left({F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)↔{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right)$
179 176 178 anbi12d ${⊢}{l}={m}\to \left(\left({x}\in \mathrm{dom}{F}\left({l}\right)\wedge {F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right)↔\left({x}\in \mathrm{dom}{F}\left({m}\right)\wedge {F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right)\right)$
180 179 rabbidva2 ${⊢}{l}={m}\to \left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}=\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}$
181 101 ineq2d ${⊢}{l}={m}\to {s}\cap \mathrm{dom}{F}\left({l}\right)={s}\cap \mathrm{dom}{F}\left({m}\right)$
182 180 181 eqeq12d ${⊢}{l}={m}\to \left(\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({l}\right)↔\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right)$
183 182 rabbidv ${⊢}{l}={m}\to \left\{{s}\in {S}|\left\{{x}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({l}\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}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
184 175 183 eqtrd ${⊢}{l}={m}\to \left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\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}{{j}}\right)\right\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right\}$
185 oveq2 ${⊢}{j}={k}\to \frac{1}{{j}}=\frac{1}{{k}}$
186 185 oveq2d ${⊢}{j}={k}\to {a}+\left(\frac{1}{{j}}\right)={a}+\left(\frac{1}{{k}}\right)$
187 186 breq2d ${⊢}{j}={k}\to \left({F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)↔{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{k}}\right)\right)$
188 187 rabbidv ${⊢}{j}={k}\to \left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}=\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{k}}\right)\right\}$
189 188 eqeq1d ${⊢}{j}={k}\to \left(\left\{{x}\in \mathrm{dom}{F}\left({m}\right)|{F}\left({m}\right)\left({x}\right)<{a}+\left(\frac{1}{{j}}\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\}={s}\cap \mathrm{dom}{F}\left({m}\right)\right)$
190 189 rabbidv ${⊢}{j}={k}\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}{{j}}\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\}$
191 184 190 sylan9eq ${⊢}\left({l}={m}\wedge {j}={k}\right)\to \left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\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\}$
192 158 159 160 161 191 cbvmpo ${⊢}\left({l}\in {Z},{j}\in ℕ⟼\left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}\right)=\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)$
193 192 eqcomi ${⊢}\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)=\left({l}\in {Z},{j}\in ℕ⟼\left\{{t}\in {S}|\left\{{y}\in \mathrm{dom}{F}\left({l}\right)|{F}\left({l}\right)\left({y}\right)<{a}+\left(\frac{1}{{j}}\right)\right\}={t}\cap \mathrm{dom}{F}\left({l}\right)\right\}\right)$
194 128 4 129 130 95 148 149 193 smflimlem6 ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{y}\in {D}|{G}\left({y}\right)\le {a}\right\}\in \left({S}{↾}_{𝑡}{D}\right)$
195 9 5 44 127 194 issmfled ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$