Metamath Proof Explorer


Theorem smfinflem

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

Proof

Step Hyp Ref Expression
1 smfinflem.m φ M
2 smfinflem.z Z = M
3 smfinflem.s φ S SAlg
4 smfinflem.f φ F : Z SMblFn S
5 smfinflem.d D = x n Z dom F n | y n Z y F n x
6 smfinflem.g G = x D sup ran n Z F n x <
7 6 a1i φ G = x D sup ran n Z F n x <
8 nfv n φ x D
9 1 2 uzn0d φ Z
10 9 adantr φ x D Z
11 3 adantr φ n Z S SAlg
12 4 ffvelrnda φ n Z F n SMblFn S
13 eqid dom F n = dom F n
14 11 12 13 smff φ n Z F n : dom F n
15 14 adantlr φ x D n Z F n : dom F n
16 ssrab2 x n Z dom F n | y n Z y F n x n Z dom F n
17 5 eleq2i x D x x n Z dom F n | y n Z y F n x
18 17 biimpi x D x x n Z dom F n | y n Z y F n x
19 16 18 sselid x D x n Z dom F n
20 19 adantr x D n Z x n Z dom F n
21 simpr x D n Z n Z
22 eliinid x n Z dom F n n Z x dom F n
23 20 21 22 syl2anc x D n Z x dom F n
24 23 adantll φ x D n Z x dom F n
25 15 24 ffvelrnd φ x D n Z F n x
26 rabidim2 x x n Z dom F n | y n Z y F n x y n Z y F n x
27 18 26 syl x D y n Z y F n x
28 27 adantl φ x D y n Z y F n x
29 8 10 25 28 infnsuprnmpt φ x D sup ran n Z F n x < = sup ran n Z F n x <
30 29 mpteq2dva φ x D sup ran n Z F n x < = x D sup ran n Z F n x <
31 7 30 eqtrd φ G = x D sup ran n Z F n x <
32 nfv x φ
33 fvex F n V
34 33 dmex dom F n V
35 34 rgenw n Z dom F n V
36 35 a1i φ n Z dom F n V
37 9 36 iinexd φ n Z dom F n V
38 5 37 rabexd φ D V
39 25 renegcld φ x D n Z F n x
40 fveq2 w = x F m w = F m x
41 40 breq2d w = x z F m w z F m x
42 41 ralbidv w = x m Z z F m w m Z z F m x
43 42 rexbidv w = x z m Z z F m w z m Z z F m x
44 nfcv _ w n Z dom F n
45 nfcv _ x Z
46 nfcv _ x F m
47 46 nfdm _ x dom F m
48 45 47 nfiin _ x m Z dom F m
49 nfv w y n Z y F n x
50 nfv x z m Z z F m w
51 nfcv _ m dom F n
52 nfcv _ n F m
53 52 nfdm _ n dom F m
54 fveq2 n = m F n = F m
55 54 dmeqd n = m dom F n = dom F m
56 51 53 55 cbviin n Z dom F n = m Z dom F m
57 56 a1i x = w n Z dom F n = m Z dom F m
58 fveq2 x = w F n x = F n w
59 58 breq2d x = w y F n x y F n w
60 59 ralbidv x = w n Z y F n x n Z y F n w
61 nfv m y F n w
62 nfcv _ n y
63 nfcv _ n
64 nfcv _ n w
65 52 64 nffv _ n F m w
66 62 63 65 nfbr n y F m w
67 54 fveq1d n = m F n w = F m w
68 67 breq2d n = m y F n w y F m w
69 61 66 68 cbvralw n Z y F n w m Z y F m w
70 69 a1i x = w n Z y F n w m Z y F m w
71 60 70 bitrd x = w n Z y F n x m Z y F m w
72 71 rexbidv x = w y n Z y F n x y m Z y F m w
73 breq1 y = z y F m w z F m w
74 73 ralbidv y = z m Z y F m w m Z z F m w
75 74 cbvrexvw y m Z y F m w z m Z z F m w
76 75 a1i x = w y m Z y F m w z m Z z F m w
77 72 76 bitrd x = w y n Z y F n x z m Z z F m w
78 44 48 49 50 57 77 cbvrabcsfw x n Z dom F n | y n Z y F n x = w m Z dom F m | z m Z z F m w
79 5 78 eqtri D = w m Z dom F m | z m Z z F m w
80 43 79 elrab2 x D x m Z dom F m z m Z z F m x
81 80 biimpi x D x m Z dom F m z m Z z F m x
82 81 simprd x D z m Z z F m x
83 82 adantl φ x D z m Z z F m x
84 renegcl z z
85 84 ad2antlr φ x D z m Z z F m x z
86 fveq2 m = n F m = F n
87 86 fveq1d m = n F m x = F n x
88 87 breq2d m = n z F m x z F n x
89 88 rspcva n Z m Z z F m x z F n x
90 89 ancoms m Z z F m x n Z z F n x
91 90 adantll φ x D z m Z z F m x n Z z F n x
92 simpllr φ x D z m Z z F m x n Z z
93 25 ad4ant14 φ x D z m Z z F m x n Z F n x
94 92 93 lenegd φ x D z m Z z F m x n Z z F n x F n x z
95 91 94 mpbid φ x D z m Z z F m x n Z F n x z
96 95 ralrimiva φ x D z m Z z F m x n Z F n x z
97 brralrspcev z n Z F n x z y n Z F n x y
98 85 96 97 syl2anc φ x D z m Z z F m x y n Z F n x y
99 98 rexlimdva2 φ x D z m Z z F m x y n Z F n x y
100 83 99 mpd φ x D y n Z F n x y
101 8 10 39 100 suprclrnmpt φ x D sup ran n Z F n x <
102 5 a1i φ D = x n Z dom F n | y n Z y F n x
103 nfv y φ x n Z dom F n
104 nfv y z n Z F n x z
105 renegcl y y
106 105 3ad2ant2 φ x n Z dom F n y n Z y F n x y
107 nfv n φ
108 nfcv _ n x
109 nfii1 _ n n Z dom F n
110 108 109 nfel n x n Z dom F n
111 107 110 nfan n φ x n Z dom F n
112 62 nfel1 n y
113 nfra1 n n Z y F n x
114 111 112 113 nf3an n φ x n Z dom F n y n Z y F n x
115 simpl2 φ x n Z dom F n y n Z y F n x n Z y
116 simpll φ x n Z dom F n n Z φ
117 simpr φ x n Z dom F n n Z n Z
118 22 adantll φ x n Z dom F n n Z x dom F n
119 14 3adant3 φ n Z x dom F n F n : dom F n
120 simp3 φ n Z x dom F n x dom F n
121 119 120 ffvelrnd φ n Z x dom F n F n x
122 116 117 118 121 syl3anc φ x n Z dom F n n Z F n x
123 122 3ad2antl1 φ x n Z dom F n y n Z y F n x n Z F n x
124 rspa n Z y F n x n Z y F n x
125 124 3ad2antl3 φ x n Z dom F n y n Z y F n x n Z y F n x
126 leneg y F n x y F n x F n x y
127 126 biimp3a y F n x y F n x F n x y
128 115 123 125 127 syl3anc φ x n Z dom F n y n Z y F n x n Z F n x y
129 128 ex φ x n Z dom F n y n Z y F n x n Z F n x y
130 114 129 ralrimi φ x n Z dom F n y n Z y F n x n Z F n x y
131 brralrspcev y n Z F n x y z n Z F n x z
132 106 130 131 syl2anc φ x n Z dom F n y n Z y F n x z n Z F n x z
133 132 3exp φ x n Z dom F n y n Z y F n x z n Z F n x z
134 103 104 133 rexlimd φ x n Z dom F n y n Z y F n x z n Z F n x z
135 84 3ad2ant2 φ x n Z dom F n z n Z F n x z z
136 nfv n z
137 nfra1 n n Z F n x z
138 111 136 137 nf3an n φ x n Z dom F n z n Z F n x z
139 122 3ad2antl1 φ x n Z dom F n z n Z F n x z n Z F n x
140 simpl2 φ x n Z dom F n z n Z F n x z n Z z
141 rspa n Z F n x z n Z F n x z
142 141 3ad2antl3 φ x n Z dom F n z n Z F n x z n Z F n x z
143 simp3 F n x z F n x z F n x z
144 renegcl F n x F n x
145 144 adantr F n x z F n x
146 simpr F n x z z
147 leneg F n x z F n x z z F n x
148 145 146 147 syl2anc F n x z F n x z z F n x
149 148 3adant3 F n x z F n x z F n x z z F n x
150 143 149 mpbid F n x z F n x z z F n x
151 recn F n x F n x
152 151 negnegd F n x F n x = F n x
153 152 3ad2ant1 F n x z F n x z F n x = F n x
154 150 153 breqtrd F n x z F n x z z F n x
155 139 140 142 154 syl3anc φ x n Z dom F n z n Z F n x z n Z z F n x
156 155 ex φ x n Z dom F n z n Z F n x z n Z z F n x
157 138 156 ralrimi φ x n Z dom F n z n Z F n x z n Z z F n x
158 breq1 y = z y F n x z F n x
159 158 ralbidv y = z n Z y F n x n Z z F n x
160 159 rspcev z n Z z F n x y n Z y F n x
161 135 157 160 syl2anc φ x n Z dom F n z n Z F n x z y n Z y F n x
162 161 3exp φ x n Z dom F n z n Z F n x z y n Z y F n x
163 162 rexlimdv φ x n Z dom F n z n Z F n x z y n Z y F n x
164 134 163 impbid φ x n Z dom F n y n Z y F n x z n Z F n x z
165 32 164 rabbida φ x n Z dom F n | y n Z y F n x = x n Z dom F n | z n Z F n x z
166 102 165 eqtrd φ D = x n Z dom F n | z n Z F n x z
167 32 166 alrimi φ x D = x n Z dom F n | z n Z F n x z
168 eqid sup ran n Z F n x < = sup ran n Z F n x <
169 168 rgenw x D sup ran n Z F n x < = sup ran n Z F n x <
170 169 a1i φ x D sup ran n Z F n x < = sup ran n Z F n x <
171 mpteq12f x D = x n Z dom F n | z n Z F n x z x D sup ran n Z F n x < = sup ran n Z F n x < x D sup ran n Z F n x < = x x n Z dom F n | z n Z F n x z sup ran n Z F n x <
172 167 170 171 syl2anc φ x D sup ran n Z F n x < = x x n Z dom F n | z n Z F n x z sup ran n Z F n x <
173 nfv z φ
174 121 renegcld φ n Z x dom F n F n x
175 nfv x φ n Z
176 34 a1i φ n Z dom F n V
177 121 3expa φ n Z x dom F n F n x
178 14 feqmptd φ n Z F n = x dom F n F n x
179 178 eqcomd φ n Z x dom F n F n x = F n
180 179 12 eqeltrd φ n Z x dom F n F n x SMblFn S
181 175 11 176 177 180 smfneg φ n Z x dom F n F n x SMblFn S
182 eqid x n Z dom F n | z n Z F n x z = x n Z dom F n | z n Z F n x z
183 eqid x x n Z dom F n | z n Z F n x z sup ran n Z F n x < = x x n Z dom F n | z n Z F n x z sup ran n Z F n x <
184 107 32 173 1 2 3 174 181 182 183 smfsupmpt φ x x n Z dom F n | z n Z F n x z sup ran n Z F n x < SMblFn S
185 172 184 eqeltrd φ x D sup ran n Z F n x < SMblFn S
186 32 3 38 101 185 smfneg φ x D sup ran n Z F n x < SMblFn S
187 31 186 eqeltrd φ G SMblFn S