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 _ m F
smflim.x _ x F
smflim.m φ M
smflim.z Z = M
smflim.s φ S SAlg
smflim.f φ F : Z SMblFn S
smflim.d D = x n Z m n dom F m | m Z F m x dom
smflim.g G = x D m Z F m x
Assertion smflim φ G SMblFn S

Proof

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