# Metamath Proof Explorer

## Theorem smflimmpt

Description: The limit of a sequence 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 ). A can contain m as a free variable, in other words it can be thought as an indexed collection A ( m ) . B can be thought as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimmpt.p ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
smflimmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
smflimmpt.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
smflimmpt.m ${⊢}{\phi }\to {M}\in ℤ$
smflimmpt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
smflimmpt.a ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {A}\in {V}$
smflimmpt.b ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in {A}\right)\to {B}\in {W}$
smflimmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smflimmpt.l ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
smflimmpt.d ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
smflimmpt.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)$
Assertion smflimmpt ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 smflimmpt.p ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
2 smflimmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 smflimmpt.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
4 smflimmpt.m ${⊢}{\phi }\to {M}\in ℤ$
5 smflimmpt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
6 smflimmpt.a ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {A}\in {V}$
7 smflimmpt.b ${⊢}\left({\phi }\wedge {m}\in {Z}\wedge {x}\in {A}\right)\to {B}\in {W}$
8 smflimmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
9 smflimmpt.l ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
10 smflimmpt.d ${⊢}{D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
11 smflimmpt.g ${⊢}{G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)$
12 11 a1i ${⊢}{\phi }\to {G}=\left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)$
13 10 a1i ${⊢}{\phi }\to {D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
14 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{n}\in {Z}$
15 1 14 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
16 5 uztrn2 ${⊢}\left({n}\in {Z}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
17 16 adantll ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
18 simpll ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {\phi }$
19 6 mptexd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
20 18 17 19 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
21 eqid ${⊢}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)=\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
22 21 fvmpt2 ${⊢}\left({m}\in {Z}\wedge \left({x}\in {A}⟼{B}\right)\in \mathrm{V}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)=\left({x}\in {A}⟼{B}\right)$
23 17 20 22 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)=\left({x}\in {A}⟼{B}\right)$
24 23 dmeqd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)=\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
25 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{n}\in {Z}$
26 2 25 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
27 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{m}\in {ℤ}_{\ge {n}}$
28 26 27 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)$
29 simplll ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\wedge {x}\in {A}\right)\to {\phi }$
30 17 adantr ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\wedge {x}\in {A}\right)\to {m}\in {Z}$
31 simpr ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\wedge {x}\in {A}\right)\to {x}\in {A}$
32 29 30 31 7 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\wedge {x}\in {A}\right)\to {B}\in {W}$
33 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
34 28 32 33 fnmptd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)Fn{A}$
35 34 fndmd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
36 24 35 eqtr2d ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {A}=\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
37 15 36 iineq2d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}=\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
38 3 37 iuneq2df ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
39 simpr ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {m}\in {Z}$
40 39 19 22 syl2anc ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)=\left({x}\in {A}⟼{B}\right)$
41 40 eqcomd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)=\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
42 41 dmeqd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)=\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
43 18 17 42 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)=\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
44 15 43 iineq2d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)=\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
45 3 44 iuneq2df ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)$
46 38 45 eqtr4d ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
47 46 eleq2d ${⊢}{\phi }\to \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}↔{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)$
48 47 biimpa ${⊢}\left({\phi }\wedge {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
49 48 adantrr ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
50 eliun ${⊢}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
51 50 biimpi ${⊢}{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
52 51 adantl ${⊢}\left({\phi }\wedge {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
53 52 adantrr ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
54 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝$
55 3 54 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
56 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
57 simpllr ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝$
58 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{x}$
59 nfii1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
60 58 59 nfel ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
61 15 60 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)$
62 5 eluzelz2 ${⊢}{n}\in {Z}\to {n}\in ℤ$
63 62 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {n}\in ℤ$
64 eqid ${⊢}{ℤ}_{\ge {n}}={ℤ}_{\ge {n}}$
65 5 fvexi ${⊢}{Z}\in \mathrm{V}$
66 65 a1i ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {Z}\in \mathrm{V}$
67 5 uzssd3 ${⊢}{n}\in {Z}\to {ℤ}_{\ge {n}}\subseteq {Z}$
68 67 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {ℤ}_{\ge {n}}\subseteq {Z}$
69 fvexd ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\in \mathrm{V}$
70 eliinid ${⊢}\left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in {A}$
71 70 adantll ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in {A}$
72 18 adantlr ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {\phi }$
73 17 adantlr ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
74 72 73 71 7 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {B}\in {W}$
75 33 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in {W}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
76 71 74 75 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
77 61 63 64 66 66 68 68 69 76 climeldmeqmpt3 ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
78 77 adantllr ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
79 57 78 mpbird ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
80 79 exp31 ${⊢}\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\to \left({n}\in {Z}\to \left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)$
81 55 56 80 rexlimd ${⊢}\left({\phi }\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)$
82 81 adantrl ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)$
83 53 82 mpd ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
84 49 83 jca ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)\to \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)$
85 84 ex ${⊢}{\phi }\to \left(\left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\to \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)$
86 47 biimpar ${⊢}\left({\phi }\wedge {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
87 86 adantrr ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
88 87 51 syl ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
89 3 56 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)$
90 simpllr ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝$
91 77 adantllr ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
92 90 91 mpbid ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\wedge {n}\in {Z}\right)\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝$
93 92 exp31 ${⊢}\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\to \left({n}\in {Z}\to \left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)$
94 89 54 93 rexlimd ${⊢}\left({\phi }\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
95 94 adantrl ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
96 88 95 mpd ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)\to \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝$
97 87 96 jca ${⊢}\left({\phi }\wedge \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)\to \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)$
98 97 ex ${⊢}{\phi }\to \left(\left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\to \left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)\right)$
99 85 98 impbid ${⊢}{\phi }\to \left(\left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\wedge \left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right)↔\left({x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\wedge \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)\right)$
100 2 99 rabbida3 ${⊢}{\phi }\to \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
101 13 100 eqtrd ${⊢}{\phi }\to {D}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
102 10 eleq2i ${⊢}{x}\in {D}↔{x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
103 102 biimpi ${⊢}{x}\in {D}\to {x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
104 rabidim1 ${⊢}{x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}\to {x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
105 103 104 51 3syl ${⊢}{x}\in {D}\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
106 105 adantl ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
107 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{x}$
108 nfiu1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}$
109 54 108 nfrabw ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}|\left({m}\in {Z}⟼{B}\right)\in \mathrm{dom}⇝\right\}$
110 10 109 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{D}$
111 107 110 nfel ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{x}\in {D}$
112 3 111 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {D}\right)$
113 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)$
114 1 14 60 nf3an ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)$
115 simp2 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {n}\in {Z}$
116 115 62 syl ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {n}\in ℤ$
117 65 a1i ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {Z}\in \mathrm{V}$
118 5 115 uzssd2 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to {ℤ}_{\ge {n}}\subseteq {Z}$
119 fvexd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\in \mathrm{V}$
120 70 3ad2antl3 ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {x}\in {A}$
121 simpl1 ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {\phi }$
122 115 16 sylan ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
123 121 122 120 7 syl3anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {B}\in {W}$
124 120 123 75 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
125 114 116 64 117 117 118 118 119 124 climfveqmpt3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\right)\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)$
126 125 3exp ${⊢}{\phi }\to \left({n}\in {Z}\to \left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)\right)$
127 126 adantr ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({n}\in {Z}\to \left({x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)\right)$
128 112 113 127 rexlimd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{m}\in {ℤ}_{\ge {n}}}{A}\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)$
129 106 128 mpd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼{B}\right)\right)$
130 129 eqcomd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to ⇝\left(\left({m}\in {Z}⟼{B}\right)\right)=⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)$
131 2 101 130 mpteq12da ${⊢}{\phi }\to \left({x}\in {D}⟼⇝\left(\left({m}\in {Z}⟼{B}\right)\right)\right)=\left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)\right)$
132 41 eqcomd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)=\left({x}\in {A}⟼{B}\right)$
133 132 fveq1d ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
134 1 133 mpteq2da ${⊢}{\phi }\to \left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)$
135 134 eqcomd ${⊢}{\phi }\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)$
136 135 eleq1d ${⊢}{\phi }\to \left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝↔\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right)$
137 2 45 136 rabbida2 ${⊢}{\phi }\to \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
138 133 eqcomd ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)=\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)$
139 1 138 mpteq2da ${⊢}{\phi }\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)=\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)$
140 139 fveq2d ${⊢}{\phi }\to ⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)=⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)$
141 2 137 140 mpteq12df ${⊢}{\phi }\to \left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\right)\right)=\left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)\right)$
142 12 131 141 3eqtrd ${⊢}{\phi }\to {G}=\left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)\right)$
143 nfmpt1 ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
144 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Z}$
145 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)$
146 144 145 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
147 1 9 21 fmptdf ${⊢}{\phi }\to \left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right):{Z}⟶\mathrm{SMblFn}\left({S}\right)$
148 eqid ${⊢}\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}$
149 eqid ${⊢}\left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)\right)=\left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)\right)$
150 143 146 4 5 8 147 148 149 smflim2 ${⊢}{\phi }\to \left({x}\in \left\{{x}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)|\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\in \mathrm{dom}⇝\right\}⟼⇝\left(\left({m}\in {Z}⟼\left({m}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({m}\right)\left({x}\right)\right)\right)\right)\in \mathrm{SMblFn}\left({S}\right)$
151 142 150 eqeltrd ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$