Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbflimsup Structured version   Unicode version

Theorem mbflimsup 21276
 Description: The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 9-May-2016.)
Hypotheses
Ref Expression
mbflimsup.1
mbflimsup.2
mbflimsup.h
mbflimsup.3
mbflimsup.4
mbflimsup.5 MblFn
mbflimsup.6
Assertion
Ref Expression
mbflimsup MblFn
Distinct variable groups:   ,,   ,   ,,   ,   ,,,
Allowed substitution hints:   ()   ()   (,)   (,,)   (,,)   (,)

Proof of Theorem mbflimsup
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbflimsup.2 . . 3
2 mbflimsup.h . . . . . 6
3 mbflimsup.1 . . . . . . . . 9
4 fvex 5808 . . . . . . . . 9
53, 4eqeltri 2538 . . . . . . . 8
65mptex 6056 . . . . . . 7
76a1i 11 . . . . . 6
8 uzssz 10990 . . . . . . . . 9
93, 8eqsstri 3493 . . . . . . . 8
10 zssre 10763 . . . . . . . 8
119, 10sstri 3472 . . . . . . 7
1211a1i 11 . . . . . 6
13 mbflimsup.3 . . . . . . . 8
143uzsup 11818 . . . . . . . 8
1513, 14syl 16 . . . . . . 7
1615adantr 465 . . . . . 6
172, 7, 12, 16limsupval2 13075 . . . . 5
18 imassrn 5287 . . . . . . 7
1913adantr 465 . . . . . . . . 9
20 mbflimsup.6 . . . . . . . . . . 11
2120anass1rs 805 . . . . . . . . . 10
22 eqid 2454 . . . . . . . . . 10
2321, 22fmptd 5975 . . . . . . . . 9
24 mbflimsup.4 . . . . . . . . . 10
25 ltpnf 11212 . . . . . . . . . 10
2624, 25syl 16 . . . . . . . . 9
272, 3limsupgre 13076 . . . . . . . . 9
2819, 23, 26, 27syl3anc 1219 . . . . . . . 8
29 frn 5672 . . . . . . . 8
3028, 29syl 16 . . . . . . 7
3118, 30syl5ss 3474 . . . . . 6
32 fdm 5670 . . . . . . . . . . 11
3328, 32syl 16 . . . . . . . . . 10
3433ineq1d 3658 . . . . . . . . 9
35 dfss1 3662 . . . . . . . . . 10
3611, 35mpbi 208 . . . . . . . . 9
3734, 36syl6eq 2511 . . . . . . . 8
38 uzid 10985 . . . . . . . . . . . 12
3913, 38syl 16 . . . . . . . . . . 11
4039, 3syl6eleqr 2553 . . . . . . . . . 10
4140adantr 465 . . . . . . . . 9
42 ne0i 3750 . . . . . . . . 9
4341, 42syl 16 . . . . . . . 8
4437, 43eqnetrd 2744 . . . . . . 7
45 imadisj 5295 . . . . . . . 8
4645necon3bii 2719 . . . . . . 7
4744, 46sylibr 212 . . . . . 6
4824leidd 10016 . . . . . . . . . 10
4921rexrd 9543 . . . . . . . . . . . 12
5049, 22fmptd 5975 . . . . . . . . . . 11
5124rexrd 9543 . . . . . . . . . . 11
522limsuple 13073 . . . . . . . . . . 11
5312, 50, 51, 52syl3anc 1219 . . . . . . . . . 10
5448, 53mpbid 210 . . . . . . . . 9
55 ssralv 3523 . . . . . . . . 9
5611, 54, 55mpsyl 63 . . . . . . . 8
572limsupgf 13070 . . . . . . . . . 10
58 ffn 5666 . . . . . . . . . 10
5957, 58ax-mp 5 . . . . . . . . 9
60 breq2 4403 . . . . . . . . . 10
6160ralima 6065 . . . . . . . . 9
6259, 12, 61sylancr 663 . . . . . . . 8
6356, 62mpbird 232 . . . . . . 7
64 breq1 4402 . . . . . . . . 9
6564ralbidv 2845 . . . . . . . 8
6665rspcev 3177 . . . . . . 7
6724, 63, 66syl2anc 661 . . . . . 6
68 infmxrre 11408 . . . . . 6
6931, 47, 67, 68syl3anc 1219 . . . . 5
70 df-ima 4960 . . . . . . 7
7128feqmptd 5852 . . . . . . . . . . 11
7271reseq1d 5216 . . . . . . . . . 10
73 resmpt 5263 . . . . . . . . . . 11
7411, 73ax-mp 5 . . . . . . . . . 10
7572, 74syl6eq 2511 . . . . . . . . 9
76 simplll 757 . . . . . . . . . . . . . . . . . . 19
773uztrn2 10988 . . . . . . . . . . . . . . . . . . . 20
7877adantll 713 . . . . . . . . . . . . . . . . . . 19
79 simpllr 758 . . . . . . . . . . . . . . . . . . 19
8076, 78, 79, 20syl12anc 1217 . . . . . . . . . . . . . . . . . 18
81 eqid 2454 . . . . . . . . . . . . . . . . . 18
8280, 81fmptd 5975 . . . . . . . . . . . . . . . . 17
83 frn 5672 . . . . . . . . . . . . . . . . 17
8482, 83syl 16 . . . . . . . . . . . . . . . 16
8584adantr 465 . . . . . . . . . . . . . . 15
86 fdm 5670 . . . . . . . . . . . . . . . . . . 19
8782, 86syl 16 . . . . . . . . . . . . . . . . . 18
88 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22
8988, 3syl6eleq 2552 . . . . . . . . . . . . . . . . . . . . 21
90 eluzelz 10980 . . . . . . . . . . . . . . . . . . . . 21
9189, 90syl 16 . . . . . . . . . . . . . . . . . . . 20
9291adantlr 714 . . . . . . . . . . . . . . . . . . 19
93 uzid 10985 . . . . . . . . . . . . . . . . . . 19
94 ne0i 3750 . . . . . . . . . . . . . . . . . . 19
9592, 93, 943syl 20 . . . . . . . . . . . . . . . . . 18
9687, 95eqnetrd 2744 . . . . . . . . . . . . . . . . 17
97 dm0rn0 5163 . . . . . . . . . . . . . . . . . 18
9897necon3bii 2719 . . . . . . . . . . . . . . . . 17
9996, 98sylib 196 . . . . . . . . . . . . . . . 16
10099adantr 465 . . . . . . . . . . . . . . 15
10111sseli 3459 . . . . . . . . . . . . . . . . . 18
102 ffvelrn 5949 . . . . . . . . . . . . . . . . . 18
10328, 101, 102syl2an 477 . . . . . . . . . . . . . . . . 17
10489adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22
105 uzss 10991 . . . . . . . . . . . . . . . . . . . . . 22
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . 21
107106, 3syl6sseqr 3510 . . . . . . . . . . . . . . . . . . . 20
108103leidd 10016 . . . . . . . . . . . . . . . . . . . . 21
10911a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
11050adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
111 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
11211, 111sseldi 3461 . . . . . . . . . . . . . . . . . . . . . 22
113103rexrd 9543 . . . . . . . . . . . . . . . . . . . . . 22
1142limsupgle 13072 . . . . . . . . . . . . . . . . . . . . . 22
115109, 110, 112, 113, 114syl211anc 1225 . . . . . . . . . . . . . . . . . . . . 21
116108, 115mpbid 210 . . . . . . . . . . . . . . . . . . . 20
117 ssralv 3523 . . . . . . . . . . . . . . . . . . . 20
118107, 116, 117sylc 60 . . . . . . . . . . . . . . . . . . 19
119107adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
120 resmpt 5263 . . . . . . . . . . . . . . . . . . . . . . . . 25
121119, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
122121fveq1d 5800 . . . . . . . . . . . . . . . . . . . . . . 23
123 fvres 5812 . . . . . . . . . . . . . . . . . . . . . . . 24
124123adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
125122, 124eqtr3d 2497 . . . . . . . . . . . . . . . . . . . . . 22
126125breq1d 4409 . . . . . . . . . . . . . . . . . . . . 21
127 eluzle 10983 . . . . . . . . . . . . . . . . . . . . . . 23
128127adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
129 biimt 335 . . . . . . . . . . . . . . . . . . . . . 22
130128, 129syl 16 . . . . . . . . . . . . . . . . . . . . 21
131126, 130bitrd 253 . . . . . . . . . . . . . . . . . . . 20
132131ralbidva 2843 . . . . . . . . . . . . . . . . . . 19
133118, 132mpbird 232 . . . . . . . . . . . . . . . . . 18
134 ffn 5666 . . . . . . . . . . . . . . . . . . 19
135 breq1 4402 . . . . . . . . . . . . . . . . . . . 20
136135ralrn 5954 . . . . . . . . . . . . . . . . . . 19
13782, 134, 1363syl 20 . . . . . . . . . . . . . . . . . 18
138133, 137mpbird 232 . . . . . . . . . . . . . . . . 17
139 breq2 4403 . . . . . . . . . . . . . . . . . . 19
140139ralbidv 2845 . . . . . . . . . . . . . . . . . 18
141140rspcev 3177 . . . . . . . . . . . . . . . . 17
142103, 138, 141syl2anc 661 . . . . . . . . . . . . . . . 16
143142adantr 465 . . . . . . . . . . . . . . 15
1449sseli 3459 . . . . . . . . . . . . . . . . . . . 20
145 eluz 10984 . . . . . . . . . . . . . . . . . . . 20
14692, 144, 145syl2an 477 . . . . . . . . . . . . . . . . . . 19
147146biimprd 223 . . . . . . . . . . . . . . . . . 18
148147impr 619 . . . . . . . . . . . . . . . . 17
149148, 125syldan 470 . . . . . . . . . . . . . . . 16
15082adantr 465 . . . . . . . . . . . . . . . . . 18
151150, 134syl 16 . . . . . . . . . . . . . . . . 17
152 fnfvelrn 5948 . . . . . . . . . . . . . . . . 17
153151, 148, 152syl2anc 661 . . . . . . . . . . . . . . . 16
154149, 153eqeltrrd 2543 . . . . . . . . . . . . . . 15
155 suprub 10401 . . . . . . . . . . . . . . 15
15685, 100, 143, 154, 155syl31anc 1222 . . . . . . . . . . . . . 14
157156expr 615 . . . . . . . . . . . . 13
158157ralrimiva 2829 . . . . . . . . . . . 12
159 suprcl 10400 . . . . . . . . . . . . . . 15
16084, 99, 142, 159syl3anc 1219 . . . . . . . . . . . . . 14
161160rexrd 9543 . . . . . . . . . . . . 13
1622limsupgle 13072 . . . . . . . . . . . . 13
163109, 110, 112, 161, 162syl211anc 1225 . . . . . . . . . . . 12
164158, 163mpbird 232 . . . . . . . . . . 11
165 suprleub 10404 . . . . . . . . . . . . 13
16684, 99, 142, 103, 165syl31anc 1222 . . . . . . . . . . . 12
167138, 166mpbird 232 . . . . . . . . . . 11
168103, 160letri3d 9626 . . . . . . . . . . 11
169164, 167, 168mpbir2and 913 . . . . . . . . . 10
170169mpteq2dva 4485 . . . . . . . . 9
17175, 170eqtrd 2495 . . . . . . . 8
172171rneqd 5174 . . . . . . 7
17370, 172syl5eq 2507 . . . . . 6
174173supeq1d 7806 . . . . 5
17517, 69, 1743eqtrd 2499 . . . 4
176175mpteq2dva 4485 . . 3
1771, 176syl5eq 2507 . 2
178 eqid 2454 . . 3
179 eqid 2454 . . . 4
180 eqid 2454 . . . 4
181 simpll 753 . . . . 5
18277adantll 713 . . . . 5
183 mbflimsup.5 . . . . 5 MblFn
184181, 182, 183syl2anc 661 . . . 4 MblFn
185 simpll 753 . . . . 5
18677ad2ant2lr 747 . . . . 5
187 simprr 756 . . . . 5
188185, 186, 187, 20syl12anc 1217 . . . 4
18980ralrimiva 2829 . . . . . . . 8
190 breq1 4402 . . . . . . . . 9
19181, 190ralrnmpt 5960 . . . . . . . 8
192189, 191syl 16 . . . . . . 7
193192rexbidv 2864 . . . . . 6
194142, 193mpbid 210 . . . . 5
195194an32s 802 . . . 4
196179, 180, 91, 184, 188, 195mbfsup 21274 . . 3 MblFn
197160an32s 802 . . . 4
198197anasss 647 . . 3
1992limsuple 13073 . . . . . . . 8
20012, 50, 51, 199syl3anc 1219 . . . . . . 7
20148, 200mpbid 210 . . . . . 6
202 ssralv 3523 . . . . . 6
20311, 201, 202mpsyl 63 . . . . 5
204169breq2d 4411 . . . . . 6
205204ralbidva 2843 . . . . 5
206203, 205mpbid 210 . . . 4
207 breq1 4402 . . . . . 6
208207ralbidv 2845 . . . . 5
209208rspcev 3177 . . . 4
21024, 206, 209syl2anc 661 . . 3
2113, 178, 13, 196, 198, 210mbfinf 21275 . 2 MblFn
212177, 211eqeltrd 2542 1 MblFn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758   wne 2647  wral 2798  wrex 2799  cvv 3076   cin 3434   wss 3435  c0 3744   class class class wbr 4399   cmpt 4457  ccnv 4946   cdm 4947   crn 4948   cres 4949  cima 4950   wfn 5520  wf 5521  cfv 5525  (class class class)co 6199  csup 7800  cr 9391   cpnf 9525  cxr 9527   clt 9528   cle 9529  cz 10756  cuz 10971  cico 11412  clsp 13065  MblFncmbf 21226 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-inf2 7957  ax-cc 8714  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469  ax-pre-sup 9470 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-disj 4370  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-se 4787  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-of 6429  df-om 6586  df-1st 6686  df-2nd 6687  df-recs 6941  df-rdg 6975  df-1o 7029  df-2o 7030  df-oadd 7033  df-omul 7034  df-er 7210  df-map 7325  df-pm 7326  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-sup 7801  df-oi 7834  df-card 8219  df-acn 8222  df-cda 8447  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-div 10104  df-nn 10433  df-2 10490  df-3 10491  df-n0 10690  df-z 10757  df-uz 10972  df-q 11064  df-rp 11102  df-xadd 11200  df-ioo 11414  df-ioc 11415  df-ico 11416  df-icc 11417  df-fz 11554  df-fzo 11665  df-fl 11758  df-seq 11923  df-exp 11982  df-hash 12220  df-cj 12705  df-re 12706  df-im 12707  df-sqr 12841  df-abs 12842  df-limsup 13066  df-clim 13083  df-rlim 13084  df-sum 13281  df-xmet 17934  df-met 17935  df-ovol 21079  df-vol 21080  df-mbf 21231 This theorem is referenced by:  mbflimlem  21277
 Copyright terms: Public domain W3C validator