Metamath Proof Explorer


Theorem smflimsuplem3

Description: The limit of the ( Hn ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem3.m φ M
smflimsuplem3.z Z = M
smflimsuplem3.s φ S SAlg
smflimsuplem3.f φ F : Z SMblFn S
smflimsuplem3.e E = n Z x m n dom F m | sup ran m n F m x * <
smflimsuplem3.h H = n Z x E n sup ran m n F m x * <
Assertion smflimsuplem3 φ x x k Z n k dom H n | n Z H n x dom n Z H n x SMblFn S

Proof

Step Hyp Ref Expression
1 smflimsuplem3.m φ M
2 smflimsuplem3.z Z = M
3 smflimsuplem3.s φ S SAlg
4 smflimsuplem3.f φ F : Z SMblFn S
5 smflimsuplem3.e E = n Z x m n dom F m | sup ran m n F m x * <
6 smflimsuplem3.h H = n Z x E n sup ran m n F m x * <
7 nfv n φ
8 nfv x φ
9 nfv k φ
10 fvex H n V
11 10 dmex dom H n V
12 11 a1i φ n Z dom H n V
13 fvexd φ n Z x dom H n H n x V
14 3 adantr φ n Z S SAlg
15 5 a1i φ E = n Z x m n dom F m | sup ran m n F m x * <
16 eqid x m n dom F m | sup ran m n F m x * < = x m n dom F m | sup ran m n F m x * <
17 2 eluzelz2 n Z n
18 eqid n = n
19 17 18 uzn0d n Z n
20 fvex F m V
21 20 dmex dom F m V
22 21 rgenw m n dom F m V
23 22 a1i n Z m n dom F m V
24 19 23 iinexd n Z m n dom F m V
25 24 adantl φ n Z m n dom F m V
26 16 25 rabexd φ n Z x m n dom F m | sup ran m n F m x * < V
27 15 26 fvmpt2d φ n Z E n = x m n dom F m | sup ran m n F m x * <
28 fvres m n F n m = F m
29 28 eqcomd m n F m = F n m
30 29 adantl φ n Z m n F m = F n m
31 30 dmeqd φ n Z m n dom F m = dom F n m
32 31 iineq2dv φ n Z m n dom F m = m n dom F n m
33 32 eleq2d φ n Z x m n dom F m x m n dom F n m
34 29 fveq1d m n F m x = F n m x
35 34 mpteq2ia m n F m x = m n F n m x
36 35 rneqi ran m n F m x = ran m n F n m x
37 36 supeq1i sup ran m n F m x * < = sup ran m n F n m x * <
38 37 a1i φ n Z sup ran m n F m x * < = sup ran m n F n m x * <
39 38 eleq1d φ n Z sup ran m n F m x * < sup ran m n F n m x * <
40 33 39 anbi12d φ n Z x m n dom F m sup ran m n F m x * < x m n dom F n m sup ran m n F n m x * <
41 40 rabbidva2 φ n Z x m n dom F m | sup ran m n F m x * < = x m n dom F n m | sup ran m n F n m x * <
42 27 41 eqtrd φ n Z E n = x m n dom F n m | sup ran m n F n m x * <
43 42 38 mpteq12dv φ n Z x E n sup ran m n F m x * < = x x m n dom F n m | sup ran m n F n m x * < sup ran m n F n m x * <
44 nfcv _ m F n
45 nfcv _ x F n
46 17 adantl φ n Z n
47 4 adantr φ n Z F : Z SMblFn S
48 2 eleq2i n Z n M
49 48 biimpi n Z n M
50 uzss n M n M
51 49 50 syl n Z n M
52 51 2 sseqtrrdi n Z n Z
53 52 adantl φ n Z n Z
54 47 53 fssresd φ n Z F n : n SMblFn S
55 eqid x m n dom F n m | sup ran m n F n m x * < = x m n dom F n m | sup ran m n F n m x * <
56 eqid x x m n dom F n m | sup ran m n F n m x * < sup ran m n F n m x * < = x x m n dom F n m | sup ran m n F n m x * < sup ran m n F n m x * <
57 44 45 46 18 14 54 55 56 smfsupxr φ n Z x x m n dom F n m | sup ran m n F n m x * < sup ran m n F n m x * < SMblFn S
58 43 57 eqeltrd φ n Z x E n sup ran m n F m x * < SMblFn S
59 58 6 fmptd φ H : Z SMblFn S
60 59 ffvelrnda φ n Z H n SMblFn S
61 eqid dom H n = dom H n
62 14 60 61 smff φ n Z H n : dom H n
63 62 feqmptd φ n Z H n = x dom H n H n x
64 63 eqcomd φ n Z x dom H n H n x = H n
65 64 60 eqeltrd φ n Z x dom H n H n x SMblFn S
66 eqid x k Z n k dom H n | n Z H n x dom = x k Z n k dom H n | n Z H n x dom
67 eqid x x k Z n k dom H n | n Z H n x dom n Z H n x = x x k Z n k dom H n | n Z H n x dom n Z H n x
68 7 8 9 1 2 12 13 3 65 66 67 smflimmpt φ x x k Z n k dom H n | n Z H n x dom n Z H n x SMblFn S