Metamath Proof Explorer


Theorem smfsuplem1

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

Ref Expression
Hypotheses smfsuplem1.m φ M
smfsuplem1.z Z = M
smfsuplem1.s φ S SAlg
smfsuplem1.f φ F : Z SMblFn S
smfsuplem1.d D = x n Z dom F n | y n Z F n x y
smfsuplem1.g G = x D sup ran n Z F n x <
smfsuplem1.a φ A
smfsuplem1.h φ H : Z S
smfsuplem1.i φ n Z F n -1 −∞ A = H n dom F n
Assertion smfsuplem1 φ G -1 −∞ A S 𝑡 D

Proof

Step Hyp Ref Expression
1 smfsuplem1.m φ M
2 smfsuplem1.z Z = M
3 smfsuplem1.s φ S SAlg
4 smfsuplem1.f φ F : Z SMblFn S
5 smfsuplem1.d D = x n Z dom F n | y n Z F n x y
6 smfsuplem1.g G = x D sup ran n Z F n x <
7 smfsuplem1.a φ A
8 smfsuplem1.h φ H : Z S
9 smfsuplem1.i φ n Z F n -1 −∞ A = H n dom F n
10 3 adantr φ n Z S SAlg
11 4 ffvelrnda φ n Z F n SMblFn S
12 eqid dom F n = dom F n
13 10 11 12 smff φ n Z F n : dom F n
14 13 ffnd φ n Z F n Fn dom F n
15 14 adantr φ n Z x G -1 −∞ A F n Fn dom F n
16 ssrab2 x n Z dom F n | y n Z F n x y n Z dom F n
17 5 16 eqsstri D n Z dom F n
18 iinss2 n Z n Z dom F n dom F n
19 17 18 sstrid n Z D dom F n
20 19 ad2antlr φ n Z x G -1 −∞ A D dom F n
21 cnvimass G -1 −∞ A dom G
22 21 sseli x G -1 −∞ A x dom G
23 22 adantl φ n Z x G -1 −∞ A x dom G
24 nfv n φ x D
25 uzid M M M
26 1 25 syl φ M M
27 26 2 eleqtrrdi φ M Z
28 27 ne0d φ Z
29 28 adantr φ x D Z
30 13 adantlr φ x D n Z F n : dom F n
31 18 adantl x D n Z n Z dom F n dom F n
32 17 sseli x D x n Z dom F n
33 32 adantr x D n Z x n Z dom F n
34 31 33 sseldd x D n Z x dom F n
35 34 adantll φ x D n Z x dom F n
36 30 35 ffvelrnd φ x D n Z F n x
37 5 rabeq2i x D x n Z dom F n y n Z F n x y
38 37 simprbi x D y n Z F n x y
39 38 adantl φ x D y n Z F n x y
40 24 29 36 39 suprclrnmpt φ x D sup ran n Z F n x <
41 40 6 fmptd φ G : D
42 41 fdmd φ dom G = D
43 42 ad2antrr φ n Z x G -1 −∞ A dom G = D
44 23 43 eleqtrd φ n Z x G -1 −∞ A x D
45 20 44 sseldd φ n Z x G -1 −∞ A x dom F n
46 mnfxr −∞ *
47 46 a1i φ n Z x G -1 −∞ A −∞ *
48 7 rexrd φ A *
49 48 ad2antrr φ n Z x G -1 −∞ A A *
50 36 an32s φ n Z x D F n x
51 44 50 syldan φ n Z x G -1 −∞ A F n x
52 51 rexrd φ n Z x G -1 −∞ A F n x *
53 51 mnfltd φ n Z x G -1 −∞ A −∞ < F n x
54 22 adantl φ x G -1 −∞ A x dom G
55 41 ffdmd φ G : dom G
56 55 ffvelrnda φ x dom G G x
57 54 56 syldan φ x G -1 −∞ A G x
58 57 adantlr φ n Z x G -1 −∞ A G x
59 7 ad2antrr φ n Z x G -1 −∞ A A
60 an32 φ n Z x D φ x D n Z
61 60 biimpi φ n Z x D φ x D n Z
62 24 36 39 suprubrnmpt φ x D n Z F n x sup ran n Z F n x <
63 61 62 syl φ n Z x D F n x sup ran n Z F n x <
64 6 a1i φ G = x D sup ran n Z F n x <
65 64 40 fvmpt2d φ x D G x = sup ran n Z F n x <
66 65 adantlr φ n Z x D G x = sup ran n Z F n x <
67 63 66 breqtrrd φ n Z x D F n x G x
68 44 67 syldan φ n Z x G -1 −∞ A F n x G x
69 46 a1i φ x G -1 −∞ A −∞ *
70 48 adantr φ x G -1 −∞ A A *
71 simpr φ x G -1 −∞ A x G -1 −∞ A
72 41 ffnd φ G Fn D
73 elpreima G Fn D x G -1 −∞ A x D G x −∞ A
74 72 73 syl φ x G -1 −∞ A x D G x −∞ A
75 74 adantr φ x G -1 −∞ A x G -1 −∞ A x D G x −∞ A
76 71 75 mpbid φ x G -1 −∞ A x D G x −∞ A
77 76 simprd φ x G -1 −∞ A G x −∞ A
78 69 70 77 iocleubd φ x G -1 −∞ A G x A
79 78 adantlr φ n Z x G -1 −∞ A G x A
80 51 58 59 68 79 letrd φ n Z x G -1 −∞ A F n x A
81 47 49 52 53 80 eliocd φ n Z x G -1 −∞ A F n x −∞ A
82 15 45 81 elpreimad φ n Z x G -1 −∞ A x F n -1 −∞ A
83 82 ssd φ n Z G -1 −∞ A F n -1 −∞ A
84 inss1 H n dom F n H n
85 9 84 eqsstrdi φ n Z F n -1 −∞ A H n
86 83 85 sstrd φ n Z G -1 −∞ A H n
87 86 ralrimiva φ n Z G -1 −∞ A H n
88 ssiin G -1 −∞ A n Z H n n Z G -1 −∞ A H n
89 87 88 sylibr φ G -1 −∞ A n Z H n
90 21 41 fssdm φ G -1 −∞ A D
91 89 90 ssind φ G -1 −∞ A n Z H n D
92 iniin1 Z n Z H n D = n Z H n D
93 28 92 syl φ n Z H n D = n Z H n D
94 72 adantr φ x n Z H n D G Fn D
95 simpr φ x n Z H n D x n Z H n D
96 27 adantr φ x n Z H n D M Z
97 fveq2 n = M H n = H M
98 97 ineq1d n = M H n D = H M D
99 98 eleq2d n = M x H n D x H M D
100 95 96 99 eliind φ x n Z H n D x H M D
101 elinel2 x H M D x D
102 100 101 syl φ x n Z H n D x D
103 46 a1i φ x n Z H n D −∞ *
104 48 adantr φ x n Z H n D A *
105 65 40 eqeltrd φ x D G x
106 105 rexrd φ x D G x *
107 102 106 syldan φ x n Z H n D G x *
108 101 adantl φ x H M D x D
109 108 105 syldan φ x H M D G x
110 109 mnfltd φ x H M D −∞ < G x
111 100 110 syldan φ x n Z H n D −∞ < G x
112 102 65 syldan φ x n Z H n D G x = sup ran n Z F n x <
113 nfv n φ
114 nfcv _ n x
115 nfii1 _ n n Z H n D
116 114 115 nfel n x n Z H n D
117 113 116 nfan n φ x n Z H n D
118 simpll φ x n Z H n D n Z φ
119 simpr φ x n Z H n D n Z n Z
120 eliinid x n Z H n D n Z x H n D
121 120 adantll φ x n Z H n D n Z x H n D
122 elinel1 x H n D x H n
123 122 3ad2ant3 φ n Z x H n D x H n
124 elinel2 x H n D x D
125 124 adantl n Z x H n D x D
126 34 ancoms n Z x D x dom F n
127 125 126 syldan n Z x H n D x dom F n
128 127 3adant1 φ n Z x H n D x dom F n
129 123 128 elind φ n Z x H n D x H n dom F n
130 9 3adant3 φ n Z x H n D F n -1 −∞ A = H n dom F n
131 129 130 eleqtrrd φ n Z x H n D x F n -1 −∞ A
132 46 a1i φ n Z x F n -1 −∞ A −∞ *
133 48 3ad2ant1 φ n Z x F n -1 −∞ A A *
134 simp3 φ n Z x F n -1 −∞ A x F n -1 −∞ A
135 elpreima F n Fn dom F n x F n -1 −∞ A x dom F n F n x −∞ A
136 14 135 syl φ n Z x F n -1 −∞ A x dom F n F n x −∞ A
137 136 3adant3 φ n Z x F n -1 −∞ A x F n -1 −∞ A x dom F n F n x −∞ A
138 134 137 mpbid φ n Z x F n -1 −∞ A x dom F n F n x −∞ A
139 138 simprd φ n Z x F n -1 −∞ A F n x −∞ A
140 132 133 139 iocleubd φ n Z x F n -1 −∞ A F n x A
141 131 140 syld3an3 φ n Z x H n D F n x A
142 118 119 121 141 syl3anc φ x n Z H n D n Z F n x A
143 142 ex φ x n Z H n D n Z F n x A
144 117 143 ralrimi φ x n Z H n D n Z F n x A
145 28 adantr φ x n Z H n D Z
146 102 36 syldanl φ x n Z H n D n Z F n x
147 102 38 syl φ x n Z H n D y n Z F n x y
148 7 adantr φ x n Z H n D A
149 117 145 146 147 148 suprleubrnmpt φ x n Z H n D sup ran n Z F n x < A n Z F n x A
150 144 149 mpbird φ x n Z H n D sup ran n Z F n x < A
151 112 150 eqbrtrd φ x n Z H n D G x A
152 103 104 107 111 151 eliocd φ x n Z H n D G x −∞ A
153 94 102 152 elpreimad φ x n Z H n D x G -1 −∞ A
154 153 ssd φ n Z H n D G -1 −∞ A
155 93 154 eqsstrd φ n Z H n D G -1 −∞ A
156 91 155 eqssd φ G -1 −∞ A = n Z H n D
157 eqid x n Z dom F n | y n Z F n x y = x n Z dom F n | y n Z F n x y
158 fvex F n V
159 158 dmex dom F n V
160 159 rgenw n Z dom F n V
161 160 a1i φ n Z dom F n V
162 28 161 iinexd φ n Z dom F n V
163 157 162 rabexd φ x n Z dom F n | y n Z F n x y V
164 5 163 eqeltrid φ D V
165 2 uzct Z ω
166 165 a1i φ Z ω
167 8 ffvelrnda φ n Z H n S
168 3 166 28 167 saliincl φ n Z H n S
169 eqid n Z H n D = n Z H n D
170 3 164 168 169 elrestd φ n Z H n D S 𝑡 D
171 156 170 eqeltrd φ G -1 −∞ A S 𝑡 D