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 _mF
smflim.x _xF
smflim.m φM
smflim.z Z=M
smflim.s φSSAlg
smflim.f φF:ZSMblFnS
smflim.d D=xnZmndomFm|mZFmxdom
smflim.g G=xDmZFmx
Assertion smflim φGSMblFnS

Proof

Step Hyp Ref Expression
1 smflim.n _mF
2 smflim.x _xF
3 smflim.m φM
4 smflim.z Z=M
5 smflim.s φSSAlg
6 smflim.f φF:ZSMblFnS
7 smflim.d D=xnZmndomFm|mZFmxdom
8 smflim.g G=xDmZFmx
9 nfv aφ
10 nfcv _xZ
11 nfcv _xn
12 nfcv _xm
13 2 12 nffv _xFm
14 13 nfdm _xdomFm
15 11 14 nfiin _xmndomFm
16 10 15 nfiun _xnZmndomFm
17 16 ssrab2f xnZmndomFm|mZFmxdomnZmndomFm
18 7 17 eqsstri DnZmndomFm
19 18 a1i φDnZmndomFm
20 uzssz M
21 4 eleq2i nZnM
22 21 biimpi nZnM
23 20 22 sselid nZn
24 uzid nnn
25 23 24 syl nZnn
26 25 adantl φnZnn
27 5 adantr φnZSSAlg
28 6 ffvelrnda φnZFnSMblFnS
29 eqid domFn=domFn
30 27 28 29 smfdmss φnZdomFnS
31 nfcv _mn
32 1 31 nffv _mFn
33 32 nfdm _mdomFn
34 nfcv _mS
35 33 34 nfss mdomFnS
36 fveq2 m=nFm=Fn
37 36 dmeqd m=ndomFm=domFn
38 37 sseq1d m=ndomFmSdomFnS
39 35 38 rspce nndomFnSmndomFmS
40 26 30 39 syl2anc φnZmndomFmS
41 iinss mndomFmSmndomFmS
42 40 41 syl φnZmndomFmS
43 42 iunssd φnZmndomFmS
44 19 43 sstrd φDS
45 nfv mφ
46 nfcv _my
47 nfmpt1 _mmZFmx
48 nfcv _mdom
49 47 48 nfel mmZFmxdom
50 nfcv _mZ
51 nfii1 _mmndomFm
52 50 51 nfiun _mnZmndomFm
53 49 52 nfrabw _mxnZmndomFm|mZFmxdom
54 7 53 nfcxfr _mD
55 46 54 nfel myD
56 45 55 nfan mφyD
57 nfcv _wF
58 5 adantr φmZSSAlg
59 6 ffvelrnda φmZFmSMblFnS
60 eqid domFm=domFm
61 58 59 60 smff φmZFm:domFm
62 61 adantlr φyDmZFm:domFm
63 nfcv _ynZmndomFm
64 nfv ymZFmxdom
65 nfcv _xy
66 13 65 nffv _xFmy
67 10 66 nfmpt _xmZFmy
68 67 nfel1 xmZFmydom
69 fveq2 x=yFmx=Fmy
70 69 mpteq2dv x=ymZFmx=mZFmy
71 70 eleq1d x=ymZFmxdommZFmydom
72 16 63 64 68 71 cbvrabw xnZmndomFm|mZFmxdom=ynZmndomFm|mZFmydom
73 nfcv _ldomFm
74 nfcv _ml
75 1 74 nffv _mFl
76 75 nfdm _mdomFl
77 fveq2 m=lFm=Fl
78 77 dmeqd m=ldomFm=domFl
79 73 76 78 cbviin mndomFm=lndomFl
80 79 a1i n=imndomFm=lndomFl
81 fveq2 n=in=i
82 eqidd n=ilidomFl=domFl
83 81 82 iineq12dv n=ilndomFl=lidomFl
84 80 83 eqtrd n=imndomFm=lidomFl
85 84 cbviunv nZmndomFm=iZlidomFl
86 85 eleq2i ynZmndomFmyiZlidomFl
87 nfcv _lZ
88 nfcv _lFmy
89 75 46 nffv _mFly
90 77 fveq1d m=lFmy=Fly
91 50 87 88 89 90 cbvmptf mZFmy=lZFly
92 91 eleq1i mZFmydomlZFlydom
93 86 92 anbi12i ynZmndomFmmZFmydomyiZlidomFllZFlydom
94 93 rabbia2 ynZmndomFm|mZFmydom=yiZlidomFl|lZFlydom
95 7 72 94 3eqtri D=yiZlidomFl|lZFlydom
96 fveq2 y=wFly=Flw
97 96 mpteq2dv y=wlZFly=lZFlw
98 97 eleq1d y=wlZFlydomlZFlwdom
99 98 cbvrabv yiZlidomFl|lZFlydom=wiZlidomFl|lZFlwdom
100 fveq2 l=mFl=Fm
101 100 dmeqd l=mdomFl=domFm
102 76 73 101 cbviin lidomFl=midomFm
103 102 a1i iZlidomFl=midomFm
104 103 iuneq2i iZlidomFl=iZmidomFm
105 104 eleq2i wiZlidomFlwiZmidomFm
106 nfcv _mw
107 75 106 nffv _mFlw
108 nfcv _lFmw
109 100 fveq1d l=mFlw=Fmw
110 87 50 107 108 109 cbvmptf lZFlw=mZFmw
111 110 eleq1i lZFlwdommZFmwdom
112 105 111 anbi12i wiZlidomFllZFlwdomwiZmidomFmmZFmwdom
113 112 rabbia2 wiZlidomFl|lZFlwdom=wiZmidomFm|mZFmwdom
114 99 113 eqtri yiZlidomFl|lZFlydom=wiZmidomFm|mZFmwdom
115 95 114 eqtri D=wiZmidomFm|mZFmwdom
116 simpr φyDyD
117 56 1 57 4 62 115 116 fnlimfvre φyDmZFmy
118 nfrab1 _xxnZmndomFm|mZFmxdom
119 7 118 nfcxfr _xD
120 nfcv _yD
121 nfcv _ymZFmx
122 nfcv _x
123 122 67 nffv _xmZFmy
124 70 fveq2d x=ymZFmx=mZFmy
125 119 120 121 123 124 cbvmptf xDmZFmx=yDmZFmy
126 8 125 eqtri G=yDmZFmy
127 117 126 fmptd φG:D
128 3 adantr φaM
129 5 adantr φaSSAlg
130 6 adantr φaF:ZSMblFnS
131 nfcv _xl
132 2 131 nffv _xFl
133 132 65 nffv _xFly
134 10 133 nfmpt _xlZFly
135 122 134 nffv _xlZFly
136 nfcv _lFmx
137 nfcv _mx
138 75 137 nffv _mFlx
139 77 fveq1d m=lFmx=Flx
140 50 87 136 138 139 cbvmptf mZFmx=lZFlx
141 140 a1i x=ymZFmx=lZFlx
142 simpl x=ylZx=y
143 142 fveq2d x=ylZFlx=Fly
144 143 mpteq2dva x=ylZFlx=lZFly
145 141 144 eqtrd x=ymZFmx=lZFly
146 145 fveq2d x=ymZFmx=lZFly
147 119 120 121 135 146 cbvmptf xDmZFmx=yDlZFly
148 8 147 eqtri G=yDlZFly
149 simpr φaa
150 nfcv _m<
151 nfcv _ma+1j
152 89 150 151 nfbr mFly<a+1j
153 152 76 nfrabw _mydomFl|Fly<a+1j
154 nfcv _mt
155 154 76 nfin _mtdomFl
156 153 155 nfeq mydomFl|Fly<a+1j=tdomFl
157 nfcv _mS
158 156 157 nfrabw _mtS|ydomFl|Fly<a+1j=tdomFl
159 nfcv _ktS|ydomFl|Fly<a+1j=tdomFl
160 nfcv _lsS|xdomFm|Fmx<a+1k=sdomFm
161 nfcv _jsS|xdomFm|Fmx<a+1k=sdomFm
162 nfcv _ydomFl
163 132 nfdm _xdomFl
164 nfcv _x<
165 nfcv _xa+1j
166 133 164 165 nfbr xFly<a+1j
167 nfv yFlx<a+1j
168 fveq2 y=xFly=Flx
169 168 breq1d y=xFly<a+1jFlx<a+1j
170 162 163 166 167 169 cbvrabw ydomFl|Fly<a+1j=xdomFl|Flx<a+1j
171 170 a1i t=sydomFl|Fly<a+1j=xdomFl|Flx<a+1j
172 ineq1 t=stdomFl=sdomFl
173 171 172 eqeq12d t=sydomFl|Fly<a+1j=tdomFlxdomFl|Flx<a+1j=sdomFl
174 173 cbvrabv tS|ydomFl|Fly<a+1j=tdomFl=sS|xdomFl|Flx<a+1j=sdomFl
175 174 a1i l=mtS|ydomFl|Fly<a+1j=tdomFl=sS|xdomFl|Flx<a+1j=sdomFl
176 101 eleq2d l=mxdomFlxdomFm
177 100 fveq1d l=mFlx=Fmx
178 177 breq1d l=mFlx<a+1jFmx<a+1j
179 176 178 anbi12d l=mxdomFlFlx<a+1jxdomFmFmx<a+1j
180 179 rabbidva2 l=mxdomFl|Flx<a+1j=xdomFm|Fmx<a+1j
181 101 ineq2d l=msdomFl=sdomFm
182 180 181 eqeq12d l=mxdomFl|Flx<a+1j=sdomFlxdomFm|Fmx<a+1j=sdomFm
183 182 rabbidv l=msS|xdomFl|Flx<a+1j=sdomFl=sS|xdomFm|Fmx<a+1j=sdomFm
184 175 183 eqtrd l=mtS|ydomFl|Fly<a+1j=tdomFl=sS|xdomFm|Fmx<a+1j=sdomFm
185 oveq2 j=k1j=1k
186 185 oveq2d j=ka+1j=a+1k
187 186 breq2d j=kFmx<a+1jFmx<a+1k
188 187 rabbidv j=kxdomFm|Fmx<a+1j=xdomFm|Fmx<a+1k
189 188 eqeq1d j=kxdomFm|Fmx<a+1j=sdomFmxdomFm|Fmx<a+1k=sdomFm
190 189 rabbidv j=ksS|xdomFm|Fmx<a+1j=sdomFm=sS|xdomFm|Fmx<a+1k=sdomFm
191 184 190 sylan9eq l=mj=ktS|ydomFl|Fly<a+1j=tdomFl=sS|xdomFm|Fmx<a+1k=sdomFm
192 158 159 160 161 191 cbvmpo lZ,jtS|ydomFl|Fly<a+1j=tdomFl=mZ,ksS|xdomFm|Fmx<a+1k=sdomFm
193 192 eqcomi mZ,ksS|xdomFm|Fmx<a+1k=sdomFm=lZ,jtS|ydomFl|Fly<a+1j=tdomFl
194 128 4 129 130 95 148 149 193 smflimlem6 φayD|GyaS𝑡D
195 9 5 44 127 194 issmfled φGSMblFnS