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

Theorem liminfval2 41459
Description: The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypotheses
Ref Expression
liminfval2.1 𝐺 = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
liminfval2.2 (𝜑𝐹𝑉)
liminfval2.3 (𝜑𝐴 ⊆ ℝ)
liminfval2.4 (𝜑 → sup(𝐴, ℝ*, < ) = +∞)
Assertion
Ref Expression
liminfval2 (𝜑 → (lim inf‘𝐹) = sup((𝐺𝐴), ℝ*, < ))
Distinct variable group:   𝑘,𝐹
Allowed substitution hints:   𝜑(𝑘)   𝐴(𝑘)   𝐺(𝑘)   𝑉(𝑘)

Proof of Theorem liminfval2
Dummy variables 𝑛 𝑥 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 liminfval2.2 . . 3 (𝜑𝐹𝑉)
2 liminfval2.1 . . . . 5 𝐺 = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
3 oveq1 6981 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑘[,)+∞) = (𝑗[,)+∞))
43imaeq2d 5768 . . . . . . . 8 (𝑘 = 𝑗 → (𝐹 “ (𝑘[,)+∞)) = (𝐹 “ (𝑗[,)+∞)))
54ineq1d 4074 . . . . . . 7 (𝑘 = 𝑗 → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) = ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*))
65infeq1d 8732 . . . . . 6 (𝑘 = 𝑗 → inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
76cbvmptv 5026 . . . . 5 (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑗 ∈ ℝ ↦ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
82, 7eqtri 2799 . . . 4 𝐺 = (𝑗 ∈ ℝ ↦ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
98liminfval 41450 . . 3 (𝐹𝑉 → (lim inf‘𝐹) = sup(ran 𝐺, ℝ*, < ))
101, 9syl 17 . 2 (𝜑 → (lim inf‘𝐹) = sup(ran 𝐺, ℝ*, < ))
11 liminfval2.4 . . . . . . 7 (𝜑 → sup(𝐴, ℝ*, < ) = +∞)
12 liminfval2.3 . . . . . . . . 9 (𝜑𝐴 ⊆ ℝ)
1312ssrexr 41116 . . . . . . . 8 (𝜑𝐴 ⊆ ℝ*)
14 supxrunb1 12525 . . . . . . . 8 (𝐴 ⊆ ℝ* → (∀𝑛 ∈ ℝ ∃𝑥𝐴 𝑛𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
1513, 14syl 17 . . . . . . 7 (𝜑 → (∀𝑛 ∈ ℝ ∃𝑥𝐴 𝑛𝑥 ↔ sup(𝐴, ℝ*, < ) = +∞))
1611, 15mpbird 249 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℝ ∃𝑥𝐴 𝑛𝑥)
178liminfgf 41449 . . . . . . . . . . 11 𝐺:ℝ⟶ℝ*
1817ffvelrni 6673 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝐺𝑛) ∈ ℝ*)
1918ad2antlr 714 . . . . . . . . 9 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → (𝐺𝑛) ∈ ℝ*)
20 simpll 754 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → 𝜑)
21 simprl 758 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → 𝑥𝐴)
2212sselda 3857 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑥 ∈ ℝ)
2317ffvelrni 6673 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (𝐺𝑥) ∈ ℝ*)
2422, 23syl 17 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ ℝ*)
2520, 21, 24syl2anc 576 . . . . . . . . 9 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → (𝐺𝑥) ∈ ℝ*)
26 imassrn 5779 . . . . . . . . . . . 12 (𝐺𝐴) ⊆ ran 𝐺
27 frn 6348 . . . . . . . . . . . . 13 (𝐺:ℝ⟶ℝ* → ran 𝐺 ⊆ ℝ*)
2817, 27ax-mp 5 . . . . . . . . . . . 12 ran 𝐺 ⊆ ℝ*
2926, 28sstri 3866 . . . . . . . . . . 11 (𝐺𝐴) ⊆ ℝ*
30 supxrcl 12521 . . . . . . . . . . 11 ((𝐺𝐴) ⊆ ℝ* → sup((𝐺𝐴), ℝ*, < ) ∈ ℝ*)
3129, 30ax-mp 5 . . . . . . . . . 10 sup((𝐺𝐴), ℝ*, < ) ∈ ℝ*
3231a1i 11 . . . . . . . . 9 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → sup((𝐺𝐴), ℝ*, < ) ∈ ℝ*)
33 simplr 756 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → 𝑛 ∈ ℝ)
3420, 21, 22syl2anc 576 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → 𝑥 ∈ ℝ)
35 simprr 760 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → 𝑛𝑥)
36 liminfgord 41445 . . . . . . . . . . 11 ((𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛𝑥) → inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < ))
3733, 34, 35, 36syl3anc 1351 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < ))
388liminfgval 41453 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ → (𝐺𝑛) = inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))
3938ad2antlr 714 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℝ) ∧ 𝑥𝐴) → (𝐺𝑛) = inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ))
408liminfgval 41453 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐺𝑥) = inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < ))
4122, 40syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (𝐺𝑥) = inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < ))
4241adantlr 702 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℝ) ∧ 𝑥𝐴) → (𝐺𝑥) = inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < ))
4339, 42breq12d 4940 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℝ) ∧ 𝑥𝐴) → ((𝐺𝑛) ≤ (𝐺𝑥) ↔ inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < )))
4443adantrr 704 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → ((𝐺𝑛) ≤ (𝐺𝑥) ↔ inf(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*), ℝ*, < )))
4537, 44mpbird 249 . . . . . . . . 9 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → (𝐺𝑛) ≤ (𝐺𝑥))
4629a1i 11 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺𝐴) ⊆ ℝ*)
47 nfv 1873 . . . . . . . . . . . . . 14 𝑗𝜑
48 inss2 4092 . . . . . . . . . . . . . . . 16 ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ℝ*
49 infxrcl 12539 . . . . . . . . . . . . . . . 16 (((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ℝ* → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
5048, 49ax-mp 5 . . . . . . . . . . . . . . 15 inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
5150a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℝ) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
5247, 51, 8fnmptd 6317 . . . . . . . . . . . . 13 (𝜑𝐺 Fn ℝ)
5352adantr 473 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐺 Fn ℝ)
54 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑥𝐴)
5553, 22, 54fnfvimad 6819 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ (𝐺𝐴))
56 supxrub 12530 . . . . . . . . . . 11 (((𝐺𝐴) ⊆ ℝ* ∧ (𝐺𝑥) ∈ (𝐺𝐴)) → (𝐺𝑥) ≤ sup((𝐺𝐴), ℝ*, < ))
5746, 55, 56syl2anc 576 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐺𝑥) ≤ sup((𝐺𝐴), ℝ*, < ))
5820, 21, 57syl2anc 576 . . . . . . . . 9 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → (𝐺𝑥) ≤ sup((𝐺𝐴), ℝ*, < ))
5919, 25, 32, 45, 58xrletrd 12369 . . . . . . . 8 (((𝜑𝑛 ∈ ℝ) ∧ (𝑥𝐴𝑛𝑥)) → (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < ))
6059rexlimdvaa 3227 . . . . . . 7 ((𝜑𝑛 ∈ ℝ) → (∃𝑥𝐴 𝑛𝑥 → (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < )))
6160ralimdva 3124 . . . . . 6 (𝜑 → (∀𝑛 ∈ ℝ ∃𝑥𝐴 𝑛𝑥 → ∀𝑛 ∈ ℝ (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < )))
6216, 61mpd 15 . . . . 5 (𝜑 → ∀𝑛 ∈ ℝ (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < ))
63 xrltso 12348 . . . . . . . . 9 < Or ℝ*
6463infex 8748 . . . . . . . 8 inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V
6564rgenw 3097 . . . . . . 7 𝑗 ∈ ℝ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V
668fnmpt 6316 . . . . . . 7 (∀𝑗 ∈ ℝ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V → 𝐺 Fn ℝ)
6765, 66ax-mp 5 . . . . . 6 𝐺 Fn ℝ
68 breq1 4930 . . . . . . 7 (𝑥 = (𝐺𝑛) → (𝑥 ≤ sup((𝐺𝐴), ℝ*, < ) ↔ (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < )))
6968ralrn 6677 . . . . . 6 (𝐺 Fn ℝ → (∀𝑥 ∈ ran 𝐺 𝑥 ≤ sup((𝐺𝐴), ℝ*, < ) ↔ ∀𝑛 ∈ ℝ (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < )))
7067, 69ax-mp 5 . . . . 5 (∀𝑥 ∈ ran 𝐺 𝑥 ≤ sup((𝐺𝐴), ℝ*, < ) ↔ ∀𝑛 ∈ ℝ (𝐺𝑛) ≤ sup((𝐺𝐴), ℝ*, < ))
7162, 70sylibr 226 . . . 4 (𝜑 → ∀𝑥 ∈ ran 𝐺 𝑥 ≤ sup((𝐺𝐴), ℝ*, < ))
72 supxrleub 12532 . . . . 5 ((ran 𝐺 ⊆ ℝ* ∧ sup((𝐺𝐴), ℝ*, < ) ∈ ℝ*) → (sup(ran 𝐺, ℝ*, < ) ≤ sup((𝐺𝐴), ℝ*, < ) ↔ ∀𝑥 ∈ ran 𝐺 𝑥 ≤ sup((𝐺𝐴), ℝ*, < )))
7328, 31, 72mp2an 679 . . . 4 (sup(ran 𝐺, ℝ*, < ) ≤ sup((𝐺𝐴), ℝ*, < ) ↔ ∀𝑥 ∈ ran 𝐺 𝑥 ≤ sup((𝐺𝐴), ℝ*, < ))
7471, 73sylibr 226 . . 3 (𝜑 → sup(ran 𝐺, ℝ*, < ) ≤ sup((𝐺𝐴), ℝ*, < ))
7526a1i 11 . . . 4 (𝜑 → (𝐺𝐴) ⊆ ran 𝐺)
7628a1i 11 . . . 4 (𝜑 → ran 𝐺 ⊆ ℝ*)
77 supxrss 12538 . . . 4 (((𝐺𝐴) ⊆ ran 𝐺 ∧ ran 𝐺 ⊆ ℝ*) → sup((𝐺𝐴), ℝ*, < ) ≤ sup(ran 𝐺, ℝ*, < ))
7875, 76, 77syl2anc 576 . . 3 (𝜑 → sup((𝐺𝐴), ℝ*, < ) ≤ sup(ran 𝐺, ℝ*, < ))
79 supxrcl 12521 . . . . 5 (ran 𝐺 ⊆ ℝ* → sup(ran 𝐺, ℝ*, < ) ∈ ℝ*)
8028, 79ax-mp 5 . . . 4 sup(ran 𝐺, ℝ*, < ) ∈ ℝ*
81 xrletri3 12361 . . . 4 ((sup(ran 𝐺, ℝ*, < ) ∈ ℝ* ∧ sup((𝐺𝐴), ℝ*, < ) ∈ ℝ*) → (sup(ran 𝐺, ℝ*, < ) = sup((𝐺𝐴), ℝ*, < ) ↔ (sup(ran 𝐺, ℝ*, < ) ≤ sup((𝐺𝐴), ℝ*, < ) ∧ sup((𝐺𝐴), ℝ*, < ) ≤ sup(ran 𝐺, ℝ*, < ))))
8280, 31, 81mp2an 679 . . 3 (sup(ran 𝐺, ℝ*, < ) = sup((𝐺𝐴), ℝ*, < ) ↔ (sup(ran 𝐺, ℝ*, < ) ≤ sup((𝐺𝐴), ℝ*, < ) ∧ sup((𝐺𝐴), ℝ*, < ) ≤ sup(ran 𝐺, ℝ*, < )))
8374, 78, 82sylanbrc 575 . 2 (𝜑 → sup(ran 𝐺, ℝ*, < ) = sup((𝐺𝐴), ℝ*, < ))
8410, 83eqtrd 2811 1 (𝜑 → (lim inf‘𝐹) = sup((𝐺𝐴), ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wral 3085  wrex 3086  Vcvv 3412  cin 3827  wss 3828   class class class wbr 4927  cmpt 5006  ran crn 5405  cima 5407   Fn wfn 6181  wf 6182  cfv 6186  (class class class)co 6974  supcsup 8695  infcinf 8696  cr 10330  +∞cpnf 10467  *cxr 10469   < clt 10470  cle 10471  [,)cico 12553  lim infclsi 41442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-po 5323  df-so 5324  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-1st 7498  df-2nd 7499  df-er 8085  df-en 8303  df-dom 8304  df-sdom 8305  df-sup 8697  df-inf 8698  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-ico 12557  df-liminf 41443
This theorem is referenced by:  liminfresico  41462
  Copyright terms: Public domain W3C validator