Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  limsuppnfdlem Structured version   Visualization version   GIF version

Theorem limsuppnfdlem 40595
 Description: If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
limsuppnfdlem.a (𝜑𝐴 ⊆ ℝ)
limsuppnfdlem.f (𝜑𝐹:𝐴⟶ℝ*)
limsuppnfdlem.u (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
limsuppnfdlem.g 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
Assertion
Ref Expression
limsuppnfdlem (𝜑 → (lim sup‘𝐹) = +∞)
Distinct variable groups:   𝑗,𝐹,𝑘,𝑥   𝜑,𝑗,𝑘,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑗,𝑘)   𝐺(𝑥,𝑗,𝑘)

Proof of Theorem limsuppnfdlem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 limsuppnfdlem.f . . . 4 (𝜑𝐹:𝐴⟶ℝ*)
2 reex 10284 . . . . . 6 ℝ ∈ V
32a1i 11 . . . . 5 (𝜑 → ℝ ∈ V)
4 limsuppnfdlem.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
53, 4ssexd 4968 . . . 4 (𝜑𝐴 ∈ V)
61, 5fexd 39970 . . 3 (𝜑𝐹 ∈ V)
7 limsuppnfdlem.g . . . 4 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
87limsupval 14504 . . 3 (𝐹 ∈ V → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
96, 8syl 17 . 2 (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
107a1i 11 . . . . . 6 (𝜑𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )))
11 limsuppnfdlem.u . . . . . . . . . . . . 13 (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
1211r19.21bi 3079 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → ∀𝑘 ∈ ℝ ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
1312r19.21bi 3079 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
1413an32s 642 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
151ffund 6229 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → Fun 𝐹)
1615adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝐴) → Fun 𝐹)
17 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝐴) → 𝑗𝐴)
181fdmd 6234 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 = 𝐴)
1918adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝐴) → dom 𝐹 = 𝐴)
2017, 19eleqtrrd 2847 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝐴) → 𝑗 ∈ dom 𝐹)
2116, 20jca 507 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐴) → (Fun 𝐹𝑗 ∈ dom 𝐹))
2221ad4ant13 757 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (Fun 𝐹𝑗 ∈ dom 𝐹))
23 simpllr 793 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘 ∈ ℝ)
2423rexrd 10347 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘 ∈ ℝ*)
25 pnfxr 10350 . . . . . . . . . . . . . . . . . . 19 +∞ ∈ ℝ*
2625a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → +∞ ∈ ℝ*)
27 ressxr 10341 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ℝ ⊆ ℝ*)
294, 28sstrd 3773 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ⊆ ℝ*)
3029adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝐴) → 𝐴 ⊆ ℝ*)
3130, 17sseldd 3764 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝐴) → 𝑗 ∈ ℝ*)
3231ad4ant13 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 ∈ ℝ*)
33 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘𝑗)
344sselda 3763 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗𝐴) → 𝑗 ∈ ℝ)
35 ltpnf 12159 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → 𝑗 < +∞)
3634, 35syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝐴) → 𝑗 < +∞)
3736ad4ant13 757 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 < +∞)
3824, 26, 32, 33, 37elicod 12431 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 ∈ (𝑘[,)+∞))
39 funfvima 6689 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑗 ∈ dom 𝐹) → (𝑗 ∈ (𝑘[,)+∞) → (𝐹𝑗) ∈ (𝐹 “ (𝑘[,)+∞))))
4022, 38, 39sylc 65 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ (𝐹 “ (𝑘[,)+∞)))
411ffvelrnda 6553 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → (𝐹𝑗) ∈ ℝ*)
4241ad4ant13 757 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ℝ*)
4340, 42elind 3962 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
4443adantllr 710 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
4544adantrr 708 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
46 simprr 789 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → 𝑥 ≤ (𝐹𝑗))
47 nfv 2009 . . . . . . . . . . . . . 14 𝑦 𝑥 ≤ (𝐹𝑗)
48 breq2 4815 . . . . . . . . . . . . . 14 (𝑦 = (𝐹𝑗) → (𝑥𝑦𝑥 ≤ (𝐹𝑗)))
4947, 48rspce 3457 . . . . . . . . . . . . 13 (((𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ∧ 𝑥 ≤ (𝐹𝑗)) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
5045, 46, 49syl2anc 579 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
5150ex 401 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) → ((𝑘𝑗𝑥 ≤ (𝐹𝑗)) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦))
5251rexlimdva 3178 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦))
5314, 52mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
5453ralrimiva 3113 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
55 inss2 3995 . . . . . . . . . 10 ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*
5655a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℝ) → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*)
57 supxrunb3 40284 . . . . . . . . 9 (((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞))
5856, 57syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ) → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞))
5954, 58mpbid 223 . . . . . . 7 ((𝜑𝑘 ∈ ℝ) → sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞)
6059mpteq2dva 4905 . . . . . 6 (𝜑 → (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ +∞))
6110, 60eqtrd 2799 . . . . 5 (𝜑𝐺 = (𝑘 ∈ ℝ ↦ +∞))
6261rneqd 5523 . . . 4 (𝜑 → ran 𝐺 = ran (𝑘 ∈ ℝ ↦ +∞))
63 eqid 2765 . . . . 5 (𝑘 ∈ ℝ ↦ +∞) = (𝑘 ∈ ℝ ↦ +∞)
6425a1i 11 . . . . 5 ((𝜑𝑘 ∈ ℝ) → +∞ ∈ ℝ*)
65 ren0 40287 . . . . . 6 ℝ ≠ ∅
6665a1i 11 . . . . 5 (𝜑 → ℝ ≠ ∅)
6763, 64, 66rnmptc 40024 . . . 4 (𝜑 → ran (𝑘 ∈ ℝ ↦ +∞) = {+∞})
6862, 67eqtrd 2799 . . 3 (𝜑 → ran 𝐺 = {+∞})
6968infeq1d 8594 . 2 (𝜑 → inf(ran 𝐺, ℝ*, < ) = inf({+∞}, ℝ*, < ))
70 xrltso 12179 . . . . 5 < Or ℝ*
7170, 25pm3.2i 462 . . . 4 ( < Or ℝ* ∧ +∞ ∈ ℝ*)
72 infsn 8621 . . . 4 (( < Or ℝ* ∧ +∞ ∈ ℝ*) → inf({+∞}, ℝ*, < ) = +∞)
7371, 72ax-mp 5 . . 3 inf({+∞}, ℝ*, < ) = +∞
7473a1i 11 . 2 (𝜑 → inf({+∞}, ℝ*, < ) = +∞)
759, 69, 743eqtrd 2803 1 (𝜑 → (lim sup‘𝐹) = +∞)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  ∀wral 3055  ∃wrex 3056  Vcvv 3350   ∩ cin 3733   ⊆ wss 3734  ∅c0 4081  {csn 4336   class class class wbr 4811   ↦ cmpt 4890   Or wor 5199  dom cdm 5279  ran crn 5280   “ cima 5282  Fun wfun 6064  ⟶wf 6066  ‘cfv 6070  (class class class)co 6846  supcsup 8557  infcinf 8558  ℝcr 10192  +∞cpnf 10329  ℝ*cxr 10331   < clt 10332   ≤ cle 10333  [,)cico 12384  lim supclsp 14500 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271 This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-po 5200  df-so 5201  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-er 7951  df-en 8165  df-dom 8166  df-sdom 8167  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-ico 12388  df-limsup 14501 This theorem is referenced by:  limsuppnfd  40596
 Copyright terms: Public domain W3C validator