Users' Mathboxes 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