Metamath Proof Explorer


Theorem smflimsup

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsup.n _mF
smflimsup.x _xF
smflimsup.m φM
smflimsup.z Z=M
smflimsup.s φSSAlg
smflimsup.f φF:ZSMblFnS
smflimsup.d D=xnZmndomFm|lim supmZFmx
smflimsup.g G=xDlim supmZFmx
Assertion smflimsup φGSMblFnS

Proof

Step Hyp Ref Expression
1 smflimsup.n _mF
2 smflimsup.x _xF
3 smflimsup.m φM
4 smflimsup.z Z=M
5 smflimsup.s φSSAlg
6 smflimsup.f φF:ZSMblFnS
7 smflimsup.d D=xnZmndomFm|lim supmZFmx
8 smflimsup.g G=xDlim supmZFmx
9 fveq2 n=jn=j
10 9 iineq1d n=jmndomFm=mjdomFm
11 nfcv _qdomFm
12 nfcv _mq
13 1 12 nffv _mFq
14 13 nfdm _mdomFq
15 fveq2 m=qFm=Fq
16 15 dmeqd m=qdomFm=domFq
17 11 14 16 cbviin mjdomFm=qjdomFq
18 17 a1i n=jmjdomFm=qjdomFq
19 10 18 eqtrd n=jmndomFm=qjdomFq
20 19 cbviunv nZmndomFm=jZqjdomFq
21 20 eleq2i xnZmndomFmxjZqjdomFq
22 nfcv _qFmx
23 nfcv _mx
24 13 23 nffv _mFqx
25 15 fveq1d m=qFmx=Fqx
26 22 24 25 cbvmpt mZFmx=qZFqx
27 26 fveq2i lim supmZFmx=lim supqZFqx
28 27 eleq1i lim supmZFmxlim supqZFqx
29 21 28 anbi12i xnZmndomFmlim supmZFmxxjZqjdomFqlim supqZFqx
30 29 rabbia2 xnZmndomFm|lim supmZFmx=xjZqjdomFq|lim supqZFqx
31 nfcv _xZ
32 nfcv _xj
33 nfcv _xq
34 2 33 nffv _xFq
35 34 nfdm _xdomFq
36 32 35 nfiin _xqjdomFq
37 31 36 nfiun _xjZqjdomFq
38 nfcv _wjZqjdomFq
39 nfv wlim supqZFqx
40 nfcv _xlim sup
41 nfcv _xw
42 34 41 nffv _xFqw
43 31 42 nfmpt _xqZFqw
44 40 43 nffv _xlim supqZFqw
45 nfcv _x
46 44 45 nfel xlim supqZFqw
47 fveq2 x=wFqx=Fqw
48 47 mpteq2dv x=wqZFqx=qZFqw
49 48 fveq2d x=wlim supqZFqx=lim supqZFqw
50 49 eleq1d x=wlim supqZFqxlim supqZFqw
51 37 38 39 46 50 cbvrabw xjZqjdomFq|lim supqZFqx=wjZqjdomFq|lim supqZFqw
52 7 30 51 3eqtri D=wjZqjdomFq|lim supqZFqw
53 27 mpteq2i xDlim supmZFmx=xDlim supqZFqx
54 nfrab1 _xxnZmndomFm|lim supmZFmx
55 7 54 nfcxfr _xD
56 nfcv _wD
57 nfcv _wlim supqZFqx
58 55 56 57 44 49 cbvmptf xDlim supqZFqx=wDlim supqZFqw
59 8 53 58 3eqtri G=wDlim supqZFqw
60 nfcv _xi
61 60 35 nfiin _xqidomFq
62 nfcv _wqidomFq
63 nfv wsupranqiFqx*<
64 60 42 nfmpt _xqiFqw
65 64 nfrn _xranqiFqw
66 nfcv _x*
67 nfcv _x<
68 65 66 67 nfsup _xsupranqiFqw*<
69 68 45 nfel xsupranqiFqw*<
70 47 mpteq2dv x=wqiFqx=qiFqw
71 70 rneqd x=wranqiFqx=ranqiFqw
72 71 supeq1d x=wsupranqiFqx*<=supranqiFqw*<
73 72 eleq1d x=wsupranqiFqx*<supranqiFqw*<
74 61 62 63 69 73 cbvrabw xqidomFq|supranqiFqx*<=wqidomFq|supranqiFqw*<
75 74 a1i i=kxqidomFq|supranqiFqx*<=wqidomFq|supranqiFqw*<
76 fveq2 i=ki=k
77 76 iineq1d i=kqidomFq=qkdomFq
78 77 eleq2d i=kwqidomFqwqkdomFq
79 76 mpteq1d i=kqiFqw=qkFqw
80 79 rneqd i=kranqiFqw=ranqkFqw
81 80 supeq1d i=ksupranqiFqw*<=supranqkFqw*<
82 81 eleq1d i=ksupranqiFqw*<supranqkFqw*<
83 78 82 anbi12d i=kwqidomFqsupranqiFqw*<wqkdomFqsupranqkFqw*<
84 83 rabbidva2 i=kwqidomFq|supranqiFqw*<=wqkdomFq|supranqkFqw*<
85 75 84 eqtrd i=kxqidomFq|supranqiFqx*<=wqkdomFq|supranqkFqw*<
86 85 cbvmptv iZxqidomFq|supranqiFqx*<=kZwqkdomFq|supranqkFqw*<
87 fveq2 y=wFpy=Fpw
88 87 mpteq2dv y=wplFpy=plFpw
89 88 rneqd y=wranplFpy=ranplFpw
90 89 supeq1d y=wsupranplFpy*<=supranplFpw*<
91 90 cbvmptv yiZxpidomFp|supranpiFpx*<lsupranplFpy*<=wiZxpidomFp|supranpiFpx*<lsupranplFpw*<
92 fveq2 p=qFp=Fq
93 92 dmeqd p=qdomFp=domFq
94 93 cbviinv pidomFp=qidomFq
95 94 eleq2i xpidomFpxqidomFq
96 nfcv _qFpx
97 nfcv _pFq
98 nfcv _px
99 97 98 nffv _pFqx
100 92 fveq1d p=qFpx=Fqx
101 96 99 100 cbvmpt piFpx=qiFqx
102 101 rneqi ranpiFpx=ranqiFqx
103 102 supeq1i supranpiFpx*<=supranqiFqx*<
104 103 eleq1i supranpiFpx*<supranqiFqx*<
105 95 104 anbi12i xpidomFpsupranpiFpx*<xqidomFqsupranqiFqx*<
106 105 rabbia2 xpidomFp|supranpiFpx*<=xqidomFq|supranqiFqx*<
107 106 mpteq2i iZxpidomFp|supranpiFpx*<=iZxqidomFq|supranqiFqx*<
108 107 fveq1i iZxpidomFp|supranpiFpx*<l=iZxqidomFq|supranqiFqx*<l
109 92 fveq1d p=qFpw=Fqw
110 109 cbvmptv plFpw=qlFqw
111 110 rneqi ranplFpw=ranqlFqw
112 111 supeq1i supranplFpw*<=supranqlFqw*<
113 108 112 mpteq12i wiZxpidomFp|supranpiFpx*<lsupranplFpw*<=wiZxqidomFq|supranqiFqx*<lsupranqlFqw*<
114 91 113 eqtri yiZxpidomFp|supranpiFpx*<lsupranplFpy*<=wiZxqidomFq|supranqiFqx*<lsupranqlFqw*<
115 114 a1i l=kyiZxpidomFp|supranpiFpx*<lsupranplFpy*<=wiZxqidomFq|supranqiFqx*<lsupranqlFqw*<
116 fveq2 l=kiZxqidomFq|supranqiFqx*<l=iZxqidomFq|supranqiFqx*<k
117 fveq2 l=kl=k
118 117 mpteq1d l=kqlFqw=qkFqw
119 118 rneqd l=kranqlFqw=ranqkFqw
120 119 supeq1d l=ksupranqlFqw*<=supranqkFqw*<
121 116 120 mpteq12dv l=kwiZxqidomFq|supranqiFqx*<lsupranqlFqw*<=wiZxqidomFq|supranqiFqx*<ksupranqkFqw*<
122 115 121 eqtrd l=kyiZxpidomFp|supranpiFpx*<lsupranplFpy*<=wiZxqidomFq|supranqiFqx*<ksupranqkFqw*<
123 122 cbvmptv lZyiZxpidomFp|supranpiFpx*<lsupranplFpy*<=kZwiZxqidomFq|supranqiFqx*<ksupranqkFqw*<
124 3 4 5 6 52 59 86 123 smflimsuplem8 φGSMblFnS