# Metamath Proof Explorer

## Theorem smfinfmpt

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

Ref Expression
Hypotheses smfinfmpt.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
smfinfmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
smfinfmpt.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
smfinfmpt.m ${⊢}{\phi }\to {M}\in ℤ$
smfinfmpt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
smfinfmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfinfmpt.b ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to {B}\in {V}$
smfinfmpt.f ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
smfinfmpt.d ${⊢}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
smfinfmpt.g ${⊢}{G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)\right)$
Assertion smfinfmpt ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 smfinfmpt.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
2 smfinfmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 smfinfmpt.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 smfinfmpt.m ${⊢}{\phi }\to {M}\in ℤ$
5 smfinfmpt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
6 smfinfmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
7 smfinfmpt.b ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to {B}\in {V}$
8 smfinfmpt.f ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
9 smfinfmpt.d ${⊢}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
10 smfinfmpt.g ${⊢}{G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)\right)$
11 10 a1i ${⊢}{\phi }\to {G}=\left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)\right)$
12 9 a1i ${⊢}{\phi }\to {D}=\left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
13 eqidd ${⊢}{\phi }\to \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)=\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
14 13 8 fvmpt2d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)=\left({x}\in {A}⟼{B}\right)$
15 14 dmeqd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)=\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
16 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{n}$
17 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Z}$
18 16 17 nfel ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{n}\in {Z}$
19 2 18 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
20 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
21 6 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {S}\in \mathrm{SAlg}$
22 7 3expa ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {A}\right)\to {B}\in {V}$
23 19 21 22 8 smffmpt ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
24 23 fvmptelrn ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {A}\right)\to {B}\in ℝ$
25 19 20 24 dmmptdf ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
26 eqidd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {A}={A}$
27 15 25 26 3eqtrrd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {A}=\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
28 1 27 iineq2d ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{A}=\bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
29 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}{A}$
30 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)$
31 17 30 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
32 31 16 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
33 32 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
34 17 33 nfiin ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
35 29 34 rabeqf ${⊢}\bigcap _{{n}\in {Z}}{A}=\bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\to \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
36 28 35 syl ${⊢}{\phi }\to \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
37 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
38 3 37 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)$
39 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{x}$
40 nfii1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
41 39 40 nfel ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
42 1 41 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)$
43 simpll ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to {\phi }$
44 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to {n}\in {Z}$
45 eliinid ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\wedge {n}\in {Z}\right)\to {x}\in \mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
46 45 adantll ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to {x}\in \mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)$
47 27 eqcomd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)={A}$
48 47 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to \mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)={A}$
49 46 48 eleqtrd ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to {x}\in {A}$
50 14 fveq1d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
51 50 3adant3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
52 simp3 ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to {x}\in {A}$
53 20 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in {V}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
54 52 7 53 syl2anc ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
55 51 54 eqtr2d ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to {B}=\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)$
56 55 breq2d ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to \left({y}\le {B}↔{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
57 43 44 49 56 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\wedge {n}\in {Z}\right)\to \left({y}\le {B}↔{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
58 42 57 ralbida ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\to \left(\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
59 38 58 rexbid ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
60 2 59 rabbida ${⊢}{\phi }\to \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}$
61 36 60 eqtrd ${⊢}{\phi }\to \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}$
62 12 61 eqtrd ${⊢}{\phi }\to {D}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}$
63 2 62 alrimi ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}$
64 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}ℝ$
65 nfra1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}$
66 64 65 nfrex ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}$
67 nfii1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}{A}$
68 66 67 nfrab ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
69 9 68 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{D}$
70 39 69 nfel ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{x}\in {D}$
71 1 70 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {D}\right)$
72 simpll ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {\phi }$
73 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {n}\in {Z}$
74 9 eleq2i ${⊢}{x}\in {D}↔{x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
75 74 biimpi ${⊢}{x}\in {D}\to {x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}$
76 rabidim1 ${⊢}{x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}{A}|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le {B}\right\}\to {x}\in \bigcap _{{n}\in {Z}}{A}$
77 75 76 syl ${⊢}{x}\in {D}\to {x}\in \bigcap _{{n}\in {Z}}{A}$
78 77 adantr ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to {x}\in \bigcap _{{n}\in {Z}}{A}$
79 simpr ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to {n}\in {Z}$
80 eliinid ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}{A}\wedge {n}\in {Z}\right)\to {x}\in {A}$
81 78 79 80 syl2anc ${⊢}\left({x}\in {D}\wedge {n}\in {Z}\right)\to {x}\in {A}$
82 81 adantll ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {x}\in {A}$
83 55 idi ${⊢}\left({\phi }\wedge {n}\in {Z}\wedge {x}\in {A}\right)\to {B}=\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)$
84 72 73 82 83 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in {D}\right)\wedge {n}\in {Z}\right)\to {B}=\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)$
85 71 84 mpteq2da ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \left({n}\in {Z}⟼{B}\right)=\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
86 85 rneqd ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to \mathrm{ran}\left({n}\in {Z}⟼{B}\right)=\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right)$
87 86 infeq1d ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
88 87 ex ${⊢}{\phi }\to \left({x}\in {D}\to sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
89 2 88 ralrimi ${⊢}{\phi }\to \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)$
90 mpteq12f ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{D}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}\wedge \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)=sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)\to \left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)\right)=\left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
91 63 89 90 syl2anc ${⊢}{\phi }\to \left({x}\in {D}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼{B}\right),ℝ,<\right)\right)=\left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
92 11 91 eqtrd ${⊢}{\phi }\to {G}=\left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
93 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
94 eqid ${⊢}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)=\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)$
95 1 8 94 fmptdf ${⊢}{\phi }\to \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right):{Z}⟶\mathrm{SMblFn}\left({S}\right)$
96 eqid ${⊢}\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}=\left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}$
97 eqid ${⊢}\left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)=\left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)$
98 93 31 4 5 6 95 96 97 smfinf ${⊢}{\phi }\to \left({x}\in \left\{{x}\in \bigcap _{{n}\in {Z}}\mathrm{dom}\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)|\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{y}\le \left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right\}⟼sup\left(\mathrm{ran}\left({n}\in {Z}⟼\left({n}\in {Z}⟼\left({x}\in {A}⟼{B}\right)\right)\left({n}\right)\left({x}\right)\right),ℝ,<\right)\right)\in \mathrm{SMblFn}\left({S}\right)$
99 92 98 eqeltrd ${⊢}{\phi }\to {G}\in \mathrm{SMblFn}\left({S}\right)$