Metamath Proof Explorer


Theorem smfliminflem

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses smfliminflem.m φ M
smfliminflem.z Z = M
smfliminflem.s φ S SAlg
smfliminflem.f φ F : Z SMblFn S
smfliminflem.d D = x n Z m n dom F m | lim inf m Z F m x
smfliminflem.g G = x D lim inf m Z F m x
Assertion smfliminflem φ G SMblFn S

Proof

Step Hyp Ref Expression
1 smfliminflem.m φ M
2 smfliminflem.z Z = M
3 smfliminflem.s φ S SAlg
4 smfliminflem.f φ F : Z SMblFn S
5 smfliminflem.d D = x n Z m n dom F m | lim inf m Z F m x
6 smfliminflem.g G = x D lim inf m Z F m x
7 6 a1i φ G = x D lim inf m Z F m x
8 ssrab2 x n Z m n dom F m | lim inf m Z F m x n Z m n dom F m
9 5 8 eqsstri D n Z m n dom F m
10 id x D x D
11 9 10 sselid x D x n Z m n dom F m
12 eqid n Z m n dom F m = n Z m n dom F m
13 2 12 allbutfi x n Z m n dom F m n Z m n x dom F m
14 11 13 sylib x D n Z m n x dom F m
15 14 adantl φ x D n Z m n x dom F m
16 nfv m φ n Z
17 nfra1 m m n x dom F m
18 16 17 nfan m φ n Z m n x dom F m
19 2 fvexi Z V
20 19 a1i φ n Z m n x dom F m Z V
21 2 eluzelz2 n Z n
22 21 zred n Z n
23 22 ad2antlr φ n Z m n x dom F m n
24 simpll φ n Z m n x dom F m φ
25 elinel1 m Z n +∞ m Z
26 3 adantr φ m Z S SAlg
27 4 ffvelrnda φ m Z F m SMblFn S
28 eqid dom F m = dom F m
29 26 27 28 smff φ m Z F m : dom F m
30 24 25 29 syl2an φ n Z m n x dom F m m Z n +∞ F m : dom F m
31 simplr n Z m n x dom F m m Z n +∞ m n x dom F m
32 eqid n = n
33 21 adantr n Z m Z n +∞ n
34 2 25 eluzelz2d m Z n +∞ m
35 34 adantl n Z m Z n +∞ m
36 22 rexrd n Z n *
37 36 adantr n Z m Z n +∞ n *
38 pnfxr +∞ *
39 38 a1i n Z m Z n +∞ +∞ *
40 elinel2 m Z n +∞ m n +∞
41 40 adantl n Z m Z n +∞ m n +∞
42 37 39 41 icogelbd n Z m Z n +∞ n m
43 32 33 35 42 eluzd n Z m Z n +∞ m n
44 43 adantlr n Z m n x dom F m m Z n +∞ m n
45 rspa m n x dom F m m n x dom F m
46 31 44 45 syl2anc n Z m n x dom F m m Z n +∞ x dom F m
47 46 adantlll φ n Z m n x dom F m m Z n +∞ x dom F m
48 30 47 ffvelrnd φ n Z m n x dom F m m Z n +∞ F m x
49 18 20 23 48 liminfval4 φ n Z m n x dom F m lim inf m Z F m x = lim sup m Z F m x
50 49 rexlimdva2 φ n Z m n x dom F m lim inf m Z F m x = lim sup m Z F m x
51 50 adantr φ x D n Z m n x dom F m lim inf m Z F m x = lim sup m Z F m x
52 15 51 mpd φ x D lim inf m Z F m x = lim sup m Z F m x
53 52 xnegeqd φ x D lim inf m Z F m x = lim sup m Z F m x
54 19 mptex m Z F m x V
55 54 limsupcli lim sup m Z F m x *
56 55 xnegnegi lim sup m Z F m x = lim sup m Z F m x
57 56 a1i φ x D lim sup m Z F m x = lim sup m Z F m x
58 53 57 eqtr2d φ x D lim sup m Z F m x = lim inf m Z F m x
59 5 rabeq2i x D x n Z m n dom F m lim inf m Z F m x
60 59 simprbi x D lim inf m Z F m x
61 60 adantl φ x D lim inf m Z F m x
62 61 rexnegd φ x D lim inf m Z F m x = lim inf m Z F m x
63 58 62 eqtr2d φ x D lim inf m Z F m x = lim sup m Z F m x
64 61 renegcld φ x D lim inf m Z F m x
65 63 64 eqeltrrd φ x D lim sup m Z F m x
66 65 rexnegd φ x D lim sup m Z F m x = lim sup m Z F m x
67 52 66 eqtrd φ x D lim inf m Z F m x = lim sup m Z F m x
68 67 mpteq2dva φ x D lim inf m Z F m x = x D lim sup m Z F m x
69 7 68 eqtrd φ G = x D lim sup m Z F m x
70 nfv x φ
71 21 32 uzn0d n Z n
72 fvex F m V
73 72 dmex dom F m V
74 73 rgenw m n dom F m V
75 74 a1i n Z m n dom F m V
76 iinexg n m n dom F m V m n dom F m V
77 71 75 76 syl2anc n Z m n dom F m V
78 77 rgen n Z m n dom F m V
79 iunexg Z V n Z m n dom F m V n Z m n dom F m V
80 19 78 79 mp2an n Z m n dom F m V
81 80 9 ssexi D V
82 81 a1i φ D V
83 5 a1i φ D = x n Z m n dom F m | lim inf m Z F m x
84 13 biimpi x n Z m n dom F m n Z m n x dom F m
85 50 imp φ n Z m n x dom F m lim inf m Z F m x = lim sup m Z F m x
86 84 85 sylan2 φ x n Z m n dom F m lim inf m Z F m x = lim sup m Z F m x
87 55 a1i lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim sup m Z F m x *
88 simpl lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim inf m Z F m x = lim sup m Z F m x
89 simpr lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim inf m Z F m x
90 88 89 eqeltrrd lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim sup m Z F m x
91 xnegrecl2 lim sup m Z F m x * lim sup m Z F m x lim sup m Z F m x
92 87 90 91 syl2anc lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim sup m Z F m x
93 simpl lim inf m Z F m x = lim sup m Z F m x lim sup m Z F m x lim inf m Z F m x = lim sup m Z F m x
94 xnegrecl lim sup m Z F m x lim sup m Z F m x
95 94 adantl lim inf m Z F m x = lim sup m Z F m x lim sup m Z F m x lim sup m Z F m x
96 93 95 eqeltrd lim inf m Z F m x = lim sup m Z F m x lim sup m Z F m x lim inf m Z F m x
97 92 96 impbida lim inf m Z F m x = lim sup m Z F m x lim inf m Z F m x lim sup m Z F m x
98 86 97 syl φ x n Z m n dom F m lim inf m Z F m x lim sup m Z F m x
99 98 rabbidva φ x n Z m n dom F m | lim inf m Z F m x = x n Z m n dom F m | lim sup m Z F m x
100 83 99 eqtrd φ D = x n Z m n dom F m | lim sup m Z F m x
101 70 100 mpteq1df φ x D lim sup m Z F m x = x x n Z m n dom F m | lim sup m Z F m x lim sup m Z F m x
102 nfv m φ
103 nfv n φ
104 negex F m x V
105 104 a1i φ m Z x dom F m F m x V
106 nfv x φ m Z
107 73 a1i φ m Z dom F m V
108 29 ffvelrnda φ m Z x dom F m F m x
109 29 feqmptd φ m Z F m = x dom F m F m x
110 109 27 eqeltrrd φ m Z x dom F m F m x SMblFn S
111 106 26 107 108 110 smfneg φ m Z x dom F m F m x SMblFn S
112 eqid x n Z m n dom F m | lim sup m Z F m x = x n Z m n dom F m | lim sup m Z F m x
113 eqid x x n Z m n dom F m | lim sup m Z F m x lim sup m Z F m x = x x n Z m n dom F m | lim sup m Z F m x lim sup m Z F m x
114 102 70 103 1 2 3 105 111 112 113 smflimsupmpt φ x x n Z m n dom F m | lim sup m Z F m x lim sup m Z F m x SMblFn S
115 101 114 eqeltrd φ x D lim sup m Z F m x SMblFn S
116 70 3 82 65 115 smfneg φ x D lim sup m Z F m x SMblFn S
117 69 116 eqeltrd φ G SMblFn S