# Metamath Proof Explorer

## Theorem smfsuplem1

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfsuplem1.m ${⊢}{\phi }\to {M}\in ℤ$
smfsuplem1.z ${⊢}{Z}={ℤ}_{\ge {M}}$
smfsuplem1.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfsuplem1.f ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
smfsuplem1.d ${⊢}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}$
smfsuplem1.g ${⊢}{G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
smfsuplem1.a ${⊢}{\phi }\to {A}\in ℝ$
smfsuplem1.h ${⊢}{\phi }\to {H}:{Z}⟶{S}$
smfsuplem1.i ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]={H}\left({n}\right)\cap \mathrm{dom}{F}\left({n}\right)$
Assertion smfsuplem1 ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\in \left({S}{↾}_{𝑡}{D}\right)$

### Proof

Step Hyp Ref Expression
1 smfsuplem1.m ${⊢}{\phi }\to {M}\in ℤ$
2 smfsuplem1.z ${⊢}{Z}={ℤ}_{\ge {M}}$
3 smfsuplem1.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
4 smfsuplem1.f ${⊢}{\phi }\to {F}:{Z}⟶\mathrm{SMblFn}\left({S}\right)$
5 smfsuplem1.d ${⊢}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}$
6 smfsuplem1.g ${⊢}{G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
7 smfsuplem1.a ${⊢}{\phi }\to {A}\in ℝ$
8 smfsuplem1.h ${⊢}{\phi }\to {H}:{Z}⟶{S}$
9 smfsuplem1.i ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]={H}\left({n}\right)\cap \mathrm{dom}{F}\left({n}\right)$
10 3 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {S}\in \mathrm{SAlg}$
11 4 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\in \mathrm{SMblFn}\left({S}\right)$
12 eqid ${⊢}\mathrm{dom}{F}\left({n}\right)=\mathrm{dom}{F}\left({n}\right)$
13 10 11 12 smff ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right):\mathrm{dom}{F}\left({n}\right)⟶ℝ$
14 13 ffnd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)Fn\mathrm{dom}{F}\left({n}\right)$
15 14 adantr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)Fn\mathrm{dom}{F}\left({n}\right)$
16 ssrab2 ${⊢}\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}\subseteq \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)$
17 5 16 eqsstri ${⊢}{D}\subseteq \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)$
18 iinss2 ${⊢}{n}\in {Z}\to \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)\subseteq \mathrm{dom}{F}\left({n}\right)$
19 17 18 sstrid ${⊢}{n}\in {Z}\to {D}\subseteq \mathrm{dom}{F}\left({n}\right)$
20 19 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {D}\subseteq \mathrm{dom}{F}\left({n}\right)$
21 cnvimass ${⊢}{{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq \mathrm{dom}{G}$
22 21 sseli ${⊢}{x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\to {x}\in \mathrm{dom}{G}$
23 22 adantl ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in \mathrm{dom}{G}$
24 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {D}\right)$
25 uzid ${⊢}{M}\in ℤ\to {M}\in {ℤ}_{\ge {M}}$
26 1 25 syl ${⊢}{\phi }\to {M}\in {ℤ}_{\ge {M}}$
27 26 2 eleqtrrdi ${⊢}{\phi }\to {M}\in {Z}$
28 27 ne0d ${⊢}{\phi }\to {Z}\ne \varnothing$
29 28 adantr ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {Z}\ne \varnothing$
30 13 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {F}\left({n}\right):\mathrm{dom}{F}\left({n}\right)⟶ℝ$
31 18 adantl ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)\subseteq \mathrm{dom}{F}\left({n}\right)$
32 17 sseli ${⊢}{x}\in {D}\to {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)$
33 32 adantr ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)$
34 31 33 sseldd ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
35 34 adantll ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
36 30 35 ffvelrnd ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\left({x}\right)\in ℝ$
37 5 rabeq2i ${⊢}{x}\in {D}↔\left({x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)\wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right)$
38 37 simprbi ${⊢}{x}\in {D}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}$
39 38 adantl ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}$
40 24 29 36 39 suprclrnmpt ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\in ℝ$
41 40 6 fmptd ${⊢}{\phi }\to {G}:{D}⟶ℝ$
42 41 fdmd ${⊢}{\phi }\to \mathrm{dom}{G}={D}$
43 42 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \mathrm{dom}{G}={D}$
44 23 43 eleqtrd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in {D}$
45 20 44 sseldd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
46 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
47 46 a1i ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
48 7 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
49 48 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {A}\in {ℝ}^{*}$
50 36 an32s ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)\to {F}\left({n}\right)\left({x}\right)\in ℝ$
51 44 50 syldan ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\in ℝ$
52 51 rexrd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\in {ℝ}^{*}$
53 51 mnfltd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \mathrm{-\infty }<{F}\left({n}\right)\left({x}\right)$
54 22 adantl ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in \mathrm{dom}{G}$
55 41 ffdmd ${⊢}{\phi }\to {G}:\mathrm{dom}{G}⟶ℝ$
56 55 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \mathrm{dom}{G}\right)\to {G}\left({x}\right)\in ℝ$
57 54 56 syldan ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {G}\left({x}\right)\in ℝ$
58 57 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {G}\left({x}\right)\in ℝ$
59 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {A}\in ℝ$
60 an32 ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)↔\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)$
61 60 biimpi ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)\to \left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)$
62 24 36 39 suprubrnmpt ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\left({x}\right)\le sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
63 61 62 syl ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)\to {F}\left({n}\right)\left({x}\right)\le sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
64 6 a1i ${⊢}{\phi }\to {G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
65 64 40 fvmpt2d ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {G}\left({x}\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
66 65 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)\to {G}\left({x}\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
67 63 66 breqtrrd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {D}\right)\to {F}\left({n}\right)\left({x}\right)\le {G}\left({x}\right)$
68 44 67 syldan ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\le {G}\left({x}\right)$
69 46 a1i ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
70 48 adantr ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {A}\in {ℝ}^{*}$
71 simpr ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
72 41 ffnd ${⊢}{\phi }\to {G}Fn{D}$
73 elpreima ${⊢}{G}Fn{D}\to \left({x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in {D}\wedge {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
74 72 73 syl ${⊢}{\phi }\to \left({x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in {D}\wedge {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
75 74 adantr ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \left({x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in {D}\wedge {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
76 71 75 mpbid ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \left({x}\in {D}\wedge {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)$
77 76 simprd ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]$
78 69 70 77 iocleubd ${⊢}\left({\phi }\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {G}\left({x}\right)\le {A}$
79 78 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {G}\left({x}\right)\le {A}$
80 51 58 59 68 79 letrd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\le {A}$
81 47 49 52 53 80 eliocd ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]$
82 15 45 81 elpreimad ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
83 82 ssd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
84 inss1 ${⊢}{H}\left({n}\right)\cap \mathrm{dom}{F}\left({n}\right)\subseteq {H}\left({n}\right)$
85 9 84 eqsstrdi ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {H}\left({n}\right)$
86 83 85 sstrd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {H}\left({n}\right)$
87 86 ralrimiva ${⊢}{\phi }\to \forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {H}\left({n}\right)$
88 ssiin ${⊢}{{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq \bigcap _{{n}\in {Z}}{H}\left({n}\right)↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {H}\left({n}\right)$
89 87 88 sylibr ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq \bigcap _{{n}\in {Z}}{H}\left({n}\right)$
90 21 41 fssdm ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq {D}$
91 89 90 ssind ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\subseteq \bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}$
92 iniin1 ${⊢}{Z}\ne \varnothing \to \bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}=\bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)$
93 28 92 syl ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}=\bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)$
94 72 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {G}Fn{D}$
95 simpr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)$
96 27 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {M}\in {Z}$
97 fveq2 ${⊢}{n}={M}\to {H}\left({n}\right)={H}\left({M}\right)$
98 97 ineq1d ${⊢}{n}={M}\to {H}\left({n}\right)\cap {D}={H}\left({M}\right)\cap {D}$
99 98 eleq2d ${⊢}{n}={M}\to \left({x}\in \left({H}\left({n}\right)\cap {D}\right)↔{x}\in \left({H}\left({M}\right)\cap {D}\right)\right)$
100 95 96 99 eliind ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in \left({H}\left({M}\right)\cap {D}\right)$
101 elinel2 ${⊢}{x}\in \left({H}\left({M}\right)\cap {D}\right)\to {x}\in {D}$
102 100 101 syl ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in {D}$
103 46 a1i ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
104 48 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {A}\in {ℝ}^{*}$
105 65 40 eqeltrd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {G}\left({x}\right)\in ℝ$
106 105 rexrd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {G}\left({x}\right)\in {ℝ}^{*}$
107 102 106 syldan ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {G}\left({x}\right)\in {ℝ}^{*}$
108 101 adantl ${⊢}\left({\phi }\wedge {x}\in \left({H}\left({M}\right)\cap {D}\right)\right)\to {x}\in {D}$
109 108 105 syldan ${⊢}\left({\phi }\wedge {x}\in \left({H}\left({M}\right)\cap {D}\right)\right)\to {G}\left({x}\right)\in ℝ$
110 109 mnfltd ${⊢}\left({\phi }\wedge {x}\in \left({H}\left({M}\right)\cap {D}\right)\right)\to \mathrm{-\infty }<{G}\left({x}\right)$
111 100 110 syldan ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \mathrm{-\infty }<{G}\left({x}\right)$
112 102 65 syldan ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {G}\left({x}\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
113 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
114 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{x}$
115 nfii1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)$
116 114 115 nfel ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)$
117 113 116 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)$
118 simpll ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\wedge {n}\in {Z}\right)\to {\phi }$
119 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\wedge {n}\in {Z}\right)\to {n}\in {Z}$
120 eliinid ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\wedge {n}\in {Z}\right)\to {x}\in \left({H}\left({n}\right)\cap {D}\right)$
121 120 adantll ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\wedge {n}\in {Z}\right)\to {x}\in \left({H}\left({n}\right)\cap {D}\right)$
122 elinel1 ${⊢}{x}\in \left({H}\left({n}\right)\cap {D}\right)\to {x}\in {H}\left({n}\right)$
123 122 3ad2ant3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in {H}\left({n}\right)$
124 elinel2 ${⊢}{x}\in \left({H}\left({n}\right)\cap {D}\right)\to {x}\in {D}$
125 124 adantl ${⊢}\left({n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in {D}$
126 34 ancoms ${⊢}\left({n}\in {Z}\wedge {x}\in {D}\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
127 125 126 syldan ${⊢}\left({n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
128 127 3adant1 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in \mathrm{dom}{F}\left({n}\right)$
129 123 128 elind ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in \left({H}\left({n}\right)\cap \mathrm{dom}{F}\left({n}\right)\right)$
130 9 3adant3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]={H}\left({n}\right)\cap \mathrm{dom}{F}\left({n}\right)$
131 129 130 eleqtrrd ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
132 46 a1i ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
133 48 3ad2ant1 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {A}\in {ℝ}^{*}$
134 simp3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
135 elpreima ${⊢}{F}\left({n}\right)Fn\mathrm{dom}{F}\left({n}\right)\to \left({x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in \mathrm{dom}{F}\left({n}\right)\wedge {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
136 14 135 syl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in \mathrm{dom}{F}\left({n}\right)\wedge {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
137 136 3adant3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \left({x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]↔\left({x}\in \mathrm{dom}{F}\left({n}\right)\wedge {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)\right)$
138 134 137 mpbid ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to \left({x}\in \mathrm{dom}{F}\left({n}\right)\wedge {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]\right)$
139 138 simprd ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]$
140 132 133 139 iocleubd ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {{F}\left({n}\right)}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\right)\to {F}\left({n}\right)\left({x}\right)\le {A}$
141 131 140 syld3an3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in \left({H}\left({n}\right)\cap {D}\right)\right)\to {F}\left({n}\right)\left({x}\right)\le {A}$
142 118 119 121 141 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\left({x}\right)\le {A}$
143 142 ex ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \left({n}\in {Z}\to {F}\left({n}\right)\left({x}\right)\le {A}\right)$
144 117 143 ralrimi ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {A}$
145 28 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {Z}\ne \varnothing$
146 102 36 syldanl ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\left({x}\right)\in ℝ$
147 102 38 syl ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}$
148 7 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {A}\in ℝ$
149 117 145 146 147 148 suprleubrnmpt ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to \left(sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\le {A}↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {A}\right)$
150 144 149 mpbird ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼{F}\left({n}\right)\left({x}\right)\right),ℝ,<\right)\le {A}$
151 112 150 eqbrtrd ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {G}\left({x}\right)\le {A}$
152 103 104 107 111 151 eliocd ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {G}\left({x}\right)\in \left(\mathrm{-\infty },{A}\right]$
153 94 102 152 elpreimad ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\right)\to {x}\in {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
154 153 ssd ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}\left({H}\left({n}\right)\cap {D}\right)\subseteq {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
155 93 154 eqsstrd ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}\subseteq {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]$
156 91 155 eqssd ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]=\bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}$
157 eqid ${⊢}\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}$
158 fvex ${⊢}{F}\left({n}\right)\in \mathrm{V}$
159 158 dmex ${⊢}\mathrm{dom}{F}\left({n}\right)\in \mathrm{V}$
160 159 rgenw ${⊢}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({n}\right)\in \mathrm{V}$
161 160 a1i ${⊢}{\phi }\to \forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{F}\left({n}\right)\in \mathrm{V}$
162 28 161 iinexd ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)\in \mathrm{V}$
163 157 162 rabexd ${⊢}{\phi }\to \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}{F}\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)\left({x}\right)\le {y}\right\}\in \mathrm{V}$
164 5 163 eqeltrid ${⊢}{\phi }\to {D}\in \mathrm{V}$
165 2 uzct ${⊢}{Z}\preccurlyeq \mathrm{\omega }$
166 165 a1i ${⊢}{\phi }\to {Z}\preccurlyeq \mathrm{\omega }$
167 8 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {H}\left({n}\right)\in {S}$
168 3 166 28 167 saliincl ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{H}\left({n}\right)\in {S}$
169 eqid ${⊢}\bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}=\bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}$
170 3 164 168 169 elrestd ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{H}\left({n}\right)\cap {D}\in \left({S}{↾}_{𝑡}{D}\right)$
171 156 170 eqeltrd ${⊢}{\phi }\to {{G}}^{-1}\left[\left(\mathrm{-\infty },{A}\right]\right]\in \left({S}{↾}_{𝑡}{D}\right)$