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

Theorem bndth 18671
 Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to .) (Contributed by Mario Carneiro, 12-Aug-2014.)
Hypotheses
Ref Expression
bndth.1
bndth.2
bndth.3
bndth.4
Assertion
Ref Expression
bndth
Distinct variable groups:   ,,   ,   ,,   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem bndth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bndth.4 . . . . 5
2 bndth.1 . . . . . 6
3 bndth.2 . . . . . . . 8
4 retopon 18485 . . . . . . . 8 TopOn
53, 4eqeltri 2436 . . . . . . 7 TopOn
65toponunii 16887 . . . . . 6
72, 6cnf 17193 . . . . 5
81, 7syl 15 . . . 4
9 frn 5501 . . . 4
108, 9syl 15 . . 3
11 imassrn 5128 . . . . . 6
12 retopbas 18482 . . . . . . . 8
13 bastg 16921 . . . . . . . 8
1412, 13ax-mp 8 . . . . . . 7
1514, 3sseqtr4i 3297 . . . . . 6
1611, 15sstri 3274 . . . . 5
17 retop 18483 . . . . . . . 8
183, 17eqeltri 2436 . . . . . . 7
1918elexi 2882 . . . . . 6
2019elpw2 4277 . . . . 5
2116, 20mpbir 200 . . . 4
22 bndth.3 . . . . . 6
23 rncmp 17340 . . . . . 6 t
2422, 1, 23syl2anc 642 . . . . 5 t
256cmpsub 17344 . . . . . 6 t
2618, 10, 25sylancr 644 . . . . 5 t
2724, 26mpbid 201 . . . 4
28 unieq 3938 . . . . . . . 8
29 uniss 3950 . . . . . . . . . . 11
3011, 29ax-mp 8 . . . . . . . . . 10
31 unirnioo 10896 . . . . . . . . . 10
3230, 31sseqtr4i 3297 . . . . . . . . 9
33 id 19 . . . . . . . . . . . 12
34 ltp1 9741 . . . . . . . . . . . 12
35 ressxr 9023 . . . . . . . . . . . . . 14
36 peano2re 9132 . . . . . . . . . . . . . 14
3735, 36sseldi 3264 . . . . . . . . . . . . 13
38 elioomnf 10891 . . . . . . . . . . . . 13
3937, 38syl 15 . . . . . . . . . . . 12
4033, 34, 39mpbir2and 888 . . . . . . . . . . 11
41 df-ov 5984 . . . . . . . . . . . 12
42 mnfxr 10607 . . . . . . . . . . . . . . . 16
4342elexi 2882 . . . . . . . . . . . . . . 15
4443snid 3756 . . . . . . . . . . . . . 14
45 opelxpi 4824 . . . . . . . . . . . . . 14
4644, 36, 45sylancr 644 . . . . . . . . . . . . 13
47 ioof 10894 . . . . . . . . . . . . . . 15
48 ffun 5497 . . . . . . . . . . . . . . 15
4947, 48ax-mp 8 . . . . . . . . . . . . . 14
50 snssi 3857 . . . . . . . . . . . . . . . . 17
5142, 50ax-mp 8 . . . . . . . . . . . . . . . 16
52 xpss12 4895 . . . . . . . . . . . . . . . 16
5351, 35, 52mp2an 653 . . . . . . . . . . . . . . 15
5447fdmi 5500 . . . . . . . . . . . . . . 15
5553, 54sseqtr4i 3297 . . . . . . . . . . . . . 14
56 funfvima2 5874 . . . . . . . . . . . . . 14
5749, 55, 56mp2an 653 . . . . . . . . . . . . 13
5846, 57syl 15 . . . . . . . . . . . 12
5941, 58syl5eqel 2450 . . . . . . . . . . 11
60 elunii 3934 . . . . . . . . . . 11
6140, 59, 60syl2anc 642 . . . . . . . . . 10
6261ssriv 3270 . . . . . . . . 9
6332, 62eqssi 3281 . . . . . . . 8
6428, 63syl6eq 2414 . . . . . . 7
6564sseq2d 3292 . . . . . 6
66 pweq 3717 . . . . . . . 8
6766ineq1d 3457 . . . . . . 7
6867rexeqdv 2828 . . . . . 6
6965, 68imbi12d 311 . . . . 5
7069rspcv 2965 . . . 4
7121, 27, 70mpsyl 59 . . 3
7210, 71mpd 14 . 2
73 simpr 447 . . . . . . . . 9
74 elin 3446 . . . . . . . . 9
7573, 74sylib 188 . . . . . . . 8
7675adantrr 697 . . . . . . 7
7776simprd 449 . . . . . 6
7875simpld 445 . . . . . . . . 9
79 elpwi 3722 . . . . . . . . 9
8078, 79syl 15 . . . . . . . 8
8151sseli 3262 . . . . . . . . . . . . . 14
8281adantr 451 . . . . . . . . . . . . 13
8335sseli 3262 . . . . . . . . . . . . . 14
8483adantl 452 . . . . . . . . . . . . 13
85 mnflt 10615 . . . . . . . . . . . . . . . . 17
86 xrltnle 9038 . . . . . . . . . . . . . . . . . 18
8742, 83, 86sylancr 644 . . . . . . . . . . . . . . . . 17
8885, 87mpbid 201 . . . . . . . . . . . . . . . 16
8988adantl 452 . . . . . . . . . . . . . . 15
90 elsni 3753 . . . . . . . . . . . . . . . . 17
9190adantr 451 . . . . . . . . . . . . . . . 16
9291breq2d 4137 . . . . . . . . . . . . . . 15
9389, 92mtbird 292 . . . . . . . . . . . . . 14
94 ioo0 10834 . . . . . . . . . . . . . . . 16
9581, 83, 94syl2an 463 . . . . . . . . . . . . . . 15
9695necon3abid 2562 . . . . . . . . . . . . . 14
9793, 96mpbird 223 . . . . . . . . . . . . 13
98 df-ioo 10813 . . . . . . . . . . . . . 14
99 idd 21 . . . . . . . . . . . . . 14
100 xrltle 10635 . . . . . . . . . . . . . 14
101 idd 21 . . . . . . . . . . . . . 14
102 xrltle 10635 . . . . . . . . . . . . . 14
10398, 99, 100, 101, 102ixxub 10830 . . . . . . . . . . . . 13
10482, 84, 97, 103syl3anc 1183 . . . . . . . . . . . 12
105 simpr 447 . . . . . . . . . . . 12
106104, 105eqeltrd 2440 . . . . . . . . . . 11
107106rgen2 2724 . . . . . . . . . 10
108 fveq2 5632 . . . . . . . . . . . . . 14
109 df-ov 5984 . . . . . . . . . . . . . 14
110108, 109syl6eqr 2416 . . . . . . . . . . . . 13
111110supeq1d 7346 . . . . . . . . . . . 12
112111eleq1d 2432 . . . . . . . . . . 11
113112ralxp 4930 . . . . . . . . . 10
114107, 113mpbir 200 . . . . . . . . 9
115 ffn 5495 . . . . . . . . . . 11
11647, 115ax-mp 8 . . . . . . . . . 10
117 supeq1 7345 . . . . . . . . . . . 12
118117eleq1d 2432 . . . . . . . . . . 11
119118ralima 5878 . . . . . . . . . 10
120116, 53, 119mp2an 653 . . . . . . . . 9
121114, 120mpbir 200 . . . . . . . 8
122 ssralv 3323 . . . . . . . 8
12380, 121, 122ee10 1381 . . . . . . 7
124123adantrr 697 . . . . . 6
125 fimaxre3 9850 . . . . . 6
12677, 124, 125syl2anc 642 . . . . 5
127 simplrr 737 . . . . . . . . . 10
128127sselda 3266 . . . . . . . . 9
129 eluni2 3933 . . . . . . . . . 10
130 r19.29r 2769 . . . . . . . . . . . 12
131 sspwuni 4089 . . . . . . . . . . . . . . . . . . . . 21
13232, 131mpbir 200 . . . . . . . . . . . . . . . . . . . 20
133803ad2ant1 977 . . . . . . . . . . . . . . . . . . . . 21
134 simp2r 983 . . . . . . . . . . . . . . . . . . . . 21
135133, 134sseldd 3267 . . . . . . . . . . . . . . . . . . . 20
136132, 135sseldi 3264 . . . . . . . . . . . . . . . . . . 19
137 elpwi 3722 . . . . . . . . . . . . . . . . . . 19
138136, 137syl 15 . . . . . . . . . . . . . . . . . 18
139 simp3l 984 . . . . . . . . . . . . . . . . . 18
140138, 139sseldd 3267 . . . . . . . . . . . . . . . . 17
141123r19.21bi 2726 . . . . . . . . . . . . . . . . . . 19
142141adantrl 696 . . . . . . . . . . . . . . . . . 18
1431423adant3 976 . . . . . . . . . . . . . . . . 17
144 simp2l 982 . . . . . . . . . . . . . . . . 17
145138, 35syl6ss 3277 . . . . . . . . . . . . . . . . . 18
146 supxrub 10796 . . . . . . . . . . . . . . . . . 18
147145, 139, 146syl2anc 642 . . . . . . . . . . . . . . . . 17
148 simp3r 985 . . . . . . . . . . . . . . . . 17
149140, 143, 144, 147, 148letrd 9120 . . . . . . . . . . . . . . . 16
1501493expia 1154 . . . . . . . . . . . . . . 15
151150anassrs 629 . . . . . . . . . . . . . 14
152151rexlimdva 2752 . . . . . . . . . . . . 13
153152adantlrr 701 . . . . . . . . . . . 12
154130, 153syl5 28 . . . . . . . . . . 11
155154expdimp 426 . . . . . . . . . 10
156129, 155sylan2b 461 . . . . . . . . 9
157128, 156syldan 456 . . . . . . . 8
158157ralrimdva 2718 . . . . . . 7
159 ffn 5495 . . . . . . . . . 10
1608, 159syl 15 . . . . . . . . 9
161160ad2antrr 706 . . . . . . . 8
162 breq1 4128 . . . . . . . . 9
163162ralrn 5775 . . . . . . . 8
164161, 163syl 15 . . . . . . 7
165158, 164sylibd 205 . . . . . 6
166165reximdva 2740 . . . . 5
167126, 166mpd 14 . . . 4
168167expr 598 . . 3
169168rexlimdva 2752 . 2
17072, 169mpd 14 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 935   wceq 1647   wcel 1715   wne 2529  wral 2628  wrex 2629   cin 3237   wss 3238  c0 3543  cpw 3714  csn 3729  cop 3732  cuni 3929   class class class wbr 4125   cxp 4790   cdm 4792   crn 4793  cima 4795   wfun 5352   wfn 5353  wf 5354  cfv 5358  (class class class)co 5981  cfn 7006  csup 7340  cr 8883  c1 8885   caddc 8887   cmnf 9012  cxr 9013   clt 9014   cle 9015  cioo 10809   ↾t crest 13535  ctg 13552  ctop 16848  TopOnctopon 16849  ctb 16852   ccn 17171  ccmp 17330 This theorem is referenced by:  evth  18672 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-cnex 8940  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-mulcom 8948  ax-addass 8949  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1ne0 8953  ax-1rid 8954  ax-rnegex 8955  ax-rrecex 8956  ax-cnre 8957  ax-pre-lttri 8958  ax-pre-lttrn 8959  ax-pre-ltadd 8960  ax-pre-mulgt0 8961  ax-pre-sup 8962 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-reu 2635  df-rmo 2636  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-int 3965  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-tr 4216  df-eprel 4408  df-id 4412  df-po 4417  df-so 4418  df-fr 4455  df-we 4457  df-ord 4498  df-on 4499  df-lim 4500  df-suc 4501  df-om 4760  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-1st 6249  df-2nd 6250  df-riota 6446  df-recs 6530  df-rdg 6565  df-1o 6621  df-oadd 6625  df-er 6802  df-map 6917  df-en 7007  df-dom 7008  df-sdom 7009  df-fin 7010  df-fi 7312  df-sup 7341  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-sub 9186  df-neg 9187  df-div 9571  df-nn 9894  df-n0 10115  df-z 10176  df-uz 10382  df-q 10468  df-ioo 10813  df-rest 13537  df-topgen 13554  df-top 16853  df-bases 16855  df-topon 16856  df-cn 17174  df-cmp 17331
 Copyright terms: Public domain W3C validator