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 42932
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 10833 . . . . . 6 ℝ ∈ V
32a1i 11 . . . . 5 (𝜑 → ℝ ∈ V)
4 limsuppnfdlem.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
53, 4ssexd 5226 . . . 4 (𝜑𝐴 ∈ V)
61, 5fexd 7052 . . 3 (𝜑𝐹 ∈ V)
7 limsuppnfdlem.g . . . 4 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
87limsupval 15048 . . 3 (𝐹 ∈ V → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
96, 8syl 17 . 2 (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
101ffund 6558 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun 𝐹)
1110adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → Fun 𝐹)
12 simpr 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐴) → 𝑗𝐴)
131fdmd 6565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝐹 = 𝐴)
1413adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐴) → dom 𝐹 = 𝐴)
1512, 14eleqtrrd 2842 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → 𝑗 ∈ dom 𝐹)
1611, 15jca 515 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝐴) → (Fun 𝐹𝑗 ∈ dom 𝐹))
1716ad4ant13 751 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (Fun 𝐹𝑗 ∈ dom 𝐹))
18 simpllr 776 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘 ∈ ℝ)
1918rexrd 10896 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘 ∈ ℝ*)
20 pnfxr 10900 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
2120a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → +∞ ∈ ℝ*)
224ssrexr 42660 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℝ*)
2322sselda 3910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → 𝑗 ∈ ℝ*)
2423ad4ant13 751 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 ∈ ℝ*)
25 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑘𝑗)
264sselda 3910 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝐴) → 𝑗 ∈ ℝ)
2726ltpnfd 12726 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝐴) → 𝑗 < +∞)
2827ad4ant13 751 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 < +∞)
2919, 21, 24, 25, 28elicod 12998 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → 𝑗 ∈ (𝑘[,)+∞))
30 funfvima 7055 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑗 ∈ dom 𝐹) → (𝑗 ∈ (𝑘[,)+∞) → (𝐹𝑗) ∈ (𝐹 “ (𝑘[,)+∞))))
3117, 29, 30sylc 65 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ (𝐹 “ (𝑘[,)+∞)))
321ffvelrnda 6913 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝐴) → (𝐹𝑗) ∈ ℝ*)
3332ad4ant13 751 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ℝ*)
3431, 33elind 4117 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
3534adantllr 719 . . . . . . . . . . . 12 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ 𝑘𝑗) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
3635adantrr 717 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → (𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
37 simprr 773 . . . . . . . . . . 11 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → 𝑥 ≤ (𝐹𝑗))
38 breq2 5066 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑗) → (𝑥𝑦𝑥 ≤ (𝐹𝑗)))
3938rspcev 3544 . . . . . . . . . . 11 (((𝐹𝑗) ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ∧ 𝑥 ≤ (𝐹𝑗)) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
4036, 37, 39syl2anc 587 . . . . . . . . . 10 (((((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑗𝐴) ∧ (𝑘𝑗𝑥 ≤ (𝐹𝑗))) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
41 limsuppnfdlem.u . . . . . . . . . . . . 13 (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
4241r19.21bi 3131 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → ∀𝑘 ∈ ℝ ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
4342r19.21bi 3131 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
4443an32s 652 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑗𝐴 (𝑘𝑗𝑥 ≤ (𝐹𝑗)))
4540, 44r19.29a 3215 . . . . . . . . 9 (((𝜑𝑘 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
4645ralrimiva 3106 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ) → ∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦)
47 inss2 4153 . . . . . . . . 9 ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*
48 supxrunb3 42627 . . . . . . . . 9 (((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞))
4947, 48mp1i 13 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ) → (∀𝑥 ∈ ℝ ∃𝑦 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)𝑥𝑦 ↔ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞))
5046, 49mpbid 235 . . . . . . 7 ((𝜑𝑘 ∈ ℝ) → sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = +∞)
5150mpteq2dva 5159 . . . . . 6 (𝜑 → (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ +∞))
527, 51syl5eq 2791 . . . . 5 (𝜑𝐺 = (𝑘 ∈ ℝ ↦ +∞))
5352rneqd 5816 . . . 4 (𝜑 → ran 𝐺 = ran (𝑘 ∈ ℝ ↦ +∞))
54 eqid 2738 . . . . 5 (𝑘 ∈ ℝ ↦ +∞) = (𝑘 ∈ ℝ ↦ +∞)
55 ren0 42630 . . . . . 6 ℝ ≠ ∅
5655a1i 11 . . . . 5 (𝜑 → ℝ ≠ ∅)
5754, 56rnmptc 7031 . . . 4 (𝜑 → ran (𝑘 ∈ ℝ ↦ +∞) = {+∞})
5853, 57eqtrd 2778 . . 3 (𝜑 → ran 𝐺 = {+∞})
5958infeq1d 9106 . 2 (𝜑 → inf(ran 𝐺, ℝ*, < ) = inf({+∞}, ℝ*, < ))
60 xrltso 12744 . . . 4 < Or ℝ*
61 infsn 9134 . . . 4 (( < Or ℝ* ∧ +∞ ∈ ℝ*) → inf({+∞}, ℝ*, < ) = +∞)
6260, 20, 61mp2an 692 . . 3 inf({+∞}, ℝ*, < ) = +∞
6362a1i 11 . 2 (𝜑 → inf({+∞}, ℝ*, < ) = +∞)
649, 59, 633eqtrd 2782 1 (𝜑 → (lim sup‘𝐹) = +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wne 2941  wral 3062  wrex 3063  Vcvv 3415  cin 3874  wss 3875  c0 4246  {csn 4550   class class class wbr 5062  cmpt 5144   Or wor 5476  dom cdm 5560  ran crn 5561  cima 5563  Fun wfun 6383  wf 6385  cfv 6389  (class class class)co 7222  supcsup 9069  infcinf 9070  cr 10741  +∞cpnf 10877  *cxr 10879   < clt 10880  cle 10881  [,)cico 12950  lim supclsp 15044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532  ax-cnex 10798  ax-resscn 10799  ax-1cn 10800  ax-icn 10801  ax-addcl 10802  ax-addrcl 10803  ax-mulcl 10804  ax-mulrcl 10805  ax-mulcom 10806  ax-addass 10807  ax-mulass 10808  ax-distr 10809  ax-i2m1 10810  ax-1ne0 10811  ax-1rid 10812  ax-rnegex 10813  ax-rrecex 10814  ax-cnre 10815  ax-pre-lttri 10816  ax-pre-lttrn 10817  ax-pre-ltadd 10818  ax-pre-mulgt0 10819  ax-pre-sup 10820
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4829  df-iun 4915  df-br 5063  df-opab 5125  df-mpt 5145  df-id 5464  df-po 5477  df-so 5478  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-riota 7179  df-ov 7225  df-oprab 7226  df-mpo 7227  df-er 8400  df-en 8636  df-dom 8637  df-sdom 8638  df-sup 9071  df-inf 9072  df-pnf 10882  df-mnf 10883  df-xr 10884  df-ltxr 10885  df-le 10886  df-sub 11077  df-neg 11078  df-ico 12954  df-limsup 15045
This theorem is referenced by:  limsuppnfd  42933
  Copyright terms: Public domain W3C validator