Metamath Proof Explorer


Theorem smflimlem2

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem2.1 Z=M
smflimlem2.2 φSSAlg
smflimlem2.3 φF:ZSMblFnS
smflimlem2.4 D=xnZmndomFm|mZFmxdom
smflimlem2.5 G=xDmZFmx
smflimlem2.6 φA
smflimlem2.7 P=mZ,ksS|xdomFm|Fmx<A+1k=sdomFm
smflimlem2.8 H=mZ,kCmPk
smflimlem2.9 I=knZmnmHk
smflimlem2.10 φrranPCrr
Assertion smflimlem2 φxD|GxADI

Proof

Step Hyp Ref Expression
1 smflimlem2.1 Z=M
2 smflimlem2.2 φSSAlg
3 smflimlem2.3 φF:ZSMblFnS
4 smflimlem2.4 D=xnZmndomFm|mZFmxdom
5 smflimlem2.5 G=xDmZFmx
6 smflimlem2.6 φA
7 smflimlem2.7 P=mZ,ksS|xdomFm|Fmx<A+1k=sdomFm
8 smflimlem2.8 H=mZ,kCmPk
9 smflimlem2.9 I=knZmnmHk
10 smflimlem2.10 φrranPCrr
11 nfrab1 _xxnZmndomFm|mZFmxdom
12 4 11 nfcxfr _xD
13 12 ssrab2f xD|GxAD
14 13 a1i φxD|GxAD
15 simpllr φxDGxAkxD
16 ssrab2 xnZmndomFm|mZFmxdomnZmndomFm
17 4 16 eqsstri DnZmndomFm
18 17 sseli xDxnZmndomFm
19 fveq2 n=in=i
20 19 iineq1d n=imndomFm=midomFm
21 20 cbviunv nZmndomFm=iZmidomFm
22 21 eleq2i xnZmndomFmxiZmidomFm
23 eliun xiZmidomFmiZxmidomFm
24 22 23 bitri xnZmndomFmiZxmidomFm
25 18 24 sylib xDiZxmidomFm
26 15 25 syl φxDGxAkiZxmidomFm
27 nfv mφxDGxA
28 nfv mk
29 27 28 nfan mφxDGxAk
30 nfv miZ
31 29 30 nfan mφxDGxAkiZ
32 nfcv _mx
33 nfii1 _mmidomFm
34 32 33 nfel mxmidomFm
35 31 34 nfan mφxDGxAkiZxmidomFm
36 nfmpt1 _mmZFmx
37 eqid i=i
38 uzssz M
39 1 eleq2i iZiM
40 39 biimpi iZiM
41 38 40 sselid iZi
42 uzid iii
43 41 42 syl iZii
44 43 ad2antlr φxDGxAkiZxmidomFmii
45 simplll φxDiZxmidomFmmiφxD
46 45 simpld φxDiZxmidomFmmiφ
47 uzss iMiM
48 40 47 syl iZiM
49 48 1 sseqtrrdi iZiZ
50 49 sselda iZmimZ
51 50 ad4ant24 φxDiZxmidomFmmimZ
52 eliinid xmidomFmmixdomFm
53 52 adantll φxDiZxmidomFmmixdomFm
54 eqidd φmZFmx=mZFmx
55 fvexd φmZFmxV
56 54 55 fvmpt2d φmZmZFmxm=Fmx
57 56 3adant3 φmZxdomFmmZFmxm=Fmx
58 2 adantr φmZSSAlg
59 3 ffvelrnda φmZFmSMblFnS
60 eqid domFm=domFm
61 58 59 60 smff φmZFm:domFm
62 61 3adant3 φmZxdomFmFm:domFm
63 simp3 φmZxdomFmxdomFm
64 62 63 ffvelrnd φmZxdomFmFmx
65 57 64 eqeltrd φmZxdomFmmZFmxm
66 46 51 53 65 syl3anc φxDiZxmidomFmmimZFmxm
67 66 adantl3r φxDGxAiZxmidomFmmimZFmxm
68 67 adantl3r φxDGxAkiZxmidomFmmimZFmxm
69 4 eleq2i xDxxnZmndomFm|mZFmxdom
70 69 biimpi xDxxnZmndomFm|mZFmxdom
71 rabidim2 xxnZmndomFm|mZFmxdommZFmxdom
72 70 71 syl xDmZFmxdom
73 climdm mZFmxdommZFmxmZFmx
74 72 73 sylib xDmZFmxmZFmx
75 74 adantl φxDmZFmxmZFmx
76 75 73 sylibr φxDmZFmxdom
77 76 73 sylib φxDmZFmxmZFmx
78 nfcv _xF
79 simpr φxDxD
80 12 78 5 79 fnlimfv φxDGx=mZFmx
81 80 eqcomd φxDmZFmx=Gx
82 77 81 breqtrd φxDmZFmxGx
83 82 ad4antr φxDGxAkiZxmidomFmmZFmxGx
84 6 ad5antr φxDGxAkiZxmidomFmA
85 simp-4r φxDGxAkiZxmidomFmGxA
86 simpllr φxDGxAkiZxmidomFmk
87 nnrecrp k1k+
88 86 87 syl φxDGxAkiZxmidomFm1k+
89 35 36 37 44 68 83 84 85 88 climleltrp φxDGxAkiZxmidomFmnimnmZFmxmmZFmxm<A+1k
90 simp-6l φxDGxAkiZxmidomFmniφ
91 simplr φxDGxAkiZxmidomFmiZ
92 91 adantr φxDGxAkiZxmidomFmniiZ
93 simplr φxDGxAkiZxmidomFmnixmidomFm
94 simpr φxDGxAkiZxmidomFmnini
95 nfv mφ
96 95 30 34 nf3an mφiZxmidomFm
97 nfv mni
98 96 97 nfan mφiZxmidomFmni
99 simpll φiZxmidomFmnimnφiZxmidomFm
100 37 uztrn2 nimnmi
101 100 adantll φiZxmidomFmnimnmi
102 simpll2 φiZxmidomFmmimZFmxm<A+1kiZ
103 simplr φiZxmidomFmmimZFmxm<A+1kmi
104 102 103 50 syl2anc φiZxmidomFmmimZFmxm<A+1kmZ
105 simpr φiZxmidomFmmimZFmxm<A+1kmZFmxm<A+1k
106 id mZmZ
107 fvexd mZFmxV
108 eqid mZFmx=mZFmx
109 108 fvmpt2 mZFmxVmZFmxm=Fmx
110 106 107 109 syl2anc mZmZFmxm=Fmx
111 110 eqcomd mZFmx=mZFmxm
112 111 adantr mZmZFmxm<A+1kFmx=mZFmxm
113 simpr mZmZFmxm<A+1kmZFmxm<A+1k
114 112 113 eqbrtrd mZmZFmxm<A+1kFmx<A+1k
115 104 105 114 syl2anc φiZxmidomFmmimZFmxm<A+1kFmx<A+1k
116 52 3ad2antl3 φiZxmidomFmmixdomFm
117 116 adantr φiZxmidomFmmiFmx<A+1kxdomFm
118 simpr φiZxmidomFmmiFmx<A+1kFmx<A+1k
119 117 118 jca φiZxmidomFmmiFmx<A+1kxdomFmFmx<A+1k
120 rabid xxdomFm|Fmx<A+1kxdomFmFmx<A+1k
121 119 120 sylibr φiZxmidomFmmiFmx<A+1kxxdomFm|Fmx<A+1k
122 115 121 syldan φiZxmidomFmmimZFmxm<A+1kxxdomFm|Fmx<A+1k
123 122 adantrl φiZxmidomFmmimZFmxmmZFmxm<A+1kxxdomFm|Fmx<A+1k
124 123 ex φiZxmidomFmmimZFmxmmZFmxm<A+1kxxdomFm|Fmx<A+1k
125 99 101 124 syl2anc φiZxmidomFmnimnmZFmxmmZFmxm<A+1kxxdomFm|Fmx<A+1k
126 98 125 ralimdaa φiZxmidomFmnimnmZFmxmmZFmxm<A+1kmnxxdomFm|Fmx<A+1k
127 90 92 93 94 126 syl31anc φxDGxAkiZxmidomFmnimnmZFmxmmZFmxm<A+1kmnxxdomFm|Fmx<A+1k
128 127 reximdva φxDGxAkiZxmidomFmnimnmZFmxmmZFmxm<A+1knimnxxdomFm|Fmx<A+1k
129 89 128 mpd φxDGxAkiZxmidomFmnimnxxdomFm|Fmx<A+1k
130 ssrexv iZnimnxxdomFm|Fmx<A+1knZmnxxdomFm|Fmx<A+1k
131 49 130 syl iZnimnxxdomFm|Fmx<A+1knZmnxxdomFm|Fmx<A+1k
132 131 ad2antlr φxDGxAkiZxmidomFmnimnxxdomFm|Fmx<A+1knZmnxxdomFm|Fmx<A+1k
133 129 132 mpd φxDGxAkiZxmidomFmnZmnxxdomFm|Fmx<A+1k
134 133 rexlimdva2 φxDGxAkiZxmidomFmnZmnxxdomFm|Fmx<A+1k
135 26 134 mpd φxDGxAknZmnxxdomFm|Fmx<A+1k
136 nfv mφknZ
137 nfra1 mmnxxdomFm|Fmx<A+1k
138 136 137 nfan mφknZmnxxdomFm|Fmx<A+1k
139 simpll1 φknZmnxxdomFm|Fmx<A+1kmnφ
140 simpll2 φknZmnxxdomFm|Fmx<A+1kmnk
141 1 uztrn2 nZjnjZ
142 141 ssd nZnZ
143 142 sselda nZmnmZ
144 143 adantll knZmnmZ
145 144 3adantl1 φknZmnmZ
146 145 adantlr φknZmnxxdomFm|Fmx<A+1kmnmZ
147 rspa mnxxdomFm|Fmx<A+1kmnxxdomFm|Fmx<A+1k
148 147 adantll φknZmnxxdomFm|Fmx<A+1kmnxxdomFm|Fmx<A+1k
149 simp1 φkmZφ
150 simp3 φkmZmZ
151 simp2 φkmZk
152 eqid sS|xdomFm|Fmx<A+1k=sdomFm=sS|xdomFm|Fmx<A+1k=sdomFm
153 152 2 rabexd φsS|xdomFm|Fmx<A+1k=sdomFmV
154 153 ralrimivw φksS|xdomFm|Fmx<A+1k=sdomFmV
155 154 ralrimivw φmZksS|xdomFm|Fmx<A+1k=sdomFmV
156 155 3ad2ant1 φkmZmZksS|xdomFm|Fmx<A+1k=sdomFmV
157 7 elrnmpoid mZkmZksS|xdomFm|Fmx<A+1k=sdomFmVmPkranP
158 150 151 156 157 syl3anc φkmZmPkranP
159 ovex mPkV
160 eleq1 r=mPkrranPmPkranP
161 160 anbi2d r=mPkφrranPφmPkranP
162 fveq2 r=mPkCr=CmPk
163 id r=mPkr=mPk
164 162 163 eleq12d r=mPkCrrCmPkmPk
165 161 164 imbi12d r=mPkφrranPCrrφmPkranPCmPkmPk
166 159 165 10 vtocl φmPkranPCmPkmPk
167 149 158 166 syl2anc φkmZCmPkmPk
168 fvexd φkmZCmPkV
169 8 ovmpt4g mZkCmPkVmHk=CmPk
170 150 151 168 169 syl3anc φkmZmHk=CmPk
171 170 eqcomd φkmZCmPk=mHk
172 149 153 syl φkmZsS|xdomFm|Fmx<A+1k=sdomFmV
173 7 ovmpt4g mZksS|xdomFm|Fmx<A+1k=sdomFmVmPk=sS|xdomFm|Fmx<A+1k=sdomFm
174 150 151 172 173 syl3anc φkmZmPk=sS|xdomFm|Fmx<A+1k=sdomFm
175 171 174 eleq12d φkmZCmPkmPkmHksS|xdomFm|Fmx<A+1k=sdomFm
176 167 175 mpbid φkmZmHksS|xdomFm|Fmx<A+1k=sdomFm
177 ineq1 s=mHksdomFm=mHkdomFm
178 177 eqeq2d s=mHkxdomFm|Fmx<A+1k=sdomFmxdomFm|Fmx<A+1k=mHkdomFm
179 178 elrab mHksS|xdomFm|Fmx<A+1k=sdomFmmHkSxdomFm|Fmx<A+1k=mHkdomFm
180 176 179 sylib φkmZmHkSxdomFm|Fmx<A+1k=mHkdomFm
181 180 simprd φkmZxdomFm|Fmx<A+1k=mHkdomFm
182 inss1 mHkdomFmmHk
183 181 182 eqsstrdi φkmZxdomFm|Fmx<A+1kmHk
184 183 adantr φkmZxxdomFm|Fmx<A+1kxdomFm|Fmx<A+1kmHk
185 simpr φkmZxxdomFm|Fmx<A+1kxxdomFm|Fmx<A+1k
186 184 185 sseldd φkmZxxdomFm|Fmx<A+1kxmHk
187 139 140 146 148 186 syl31anc φknZmnxxdomFm|Fmx<A+1kmnxmHk
188 187 ex φknZmnxxdomFm|Fmx<A+1kmnxmHk
189 138 188 ralrimi φknZmnxxdomFm|Fmx<A+1kmnxmHk
190 vex xV
191 eliin xVxmnmHkmnxmHk
192 190 191 ax-mp xmnmHkmnxmHk
193 189 192 sylibr φknZmnxxdomFm|Fmx<A+1kxmnmHk
194 193 ex φknZmnxxdomFm|Fmx<A+1kxmnmHk
195 194 ad5ant145 φxDGxAknZmnxxdomFm|Fmx<A+1kxmnmHk
196 195 reximdva φxDGxAknZmnxxdomFm|Fmx<A+1knZxmnmHk
197 135 196 mpd φxDGxAknZxmnmHk
198 eliun xnZmnmHknZxmnmHk
199 197 198 sylibr φxDGxAkxnZmnmHk
200 199 ralrimiva φxDGxAkxnZmnmHk
201 eliin xVxknZmnmHkkxnZmnmHk
202 190 201 ax-mp xknZmnmHkkxnZmnmHk
203 200 202 sylibr φxDGxAxknZmnmHk
204 203 9 eleqtrrdi φxDGxAxI
205 204 ex φxDGxAxI
206 205 ralrimiva φxDGxAxI
207 rabss xD|GxAIxDGxAxI
208 206 207 sylibr φxD|GxAI
209 14 208 ssind φxD|GxADI