MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limsupgle Structured version   Visualization version   GIF version

Theorem limsupgle 14494
Description: The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.)
Hypothesis
Ref Expression
limsupval.1 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
Assertion
Ref Expression
limsupgle (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐺𝐶) ≤ 𝐴 ↔ ∀𝑗𝐵 (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴)))
Distinct variable groups:   𝑘,𝐹   𝐴,𝑗   𝐵,𝑗   𝐶,𝑗,𝑘   𝑗,𝐹
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)   𝐺(𝑗,𝑘)

Proof of Theorem limsupgle
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 limsupval.1 . . . . 5 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
21limsupgval 14493 . . . 4 (𝐶 ∈ ℝ → (𝐺𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*), ℝ*, < ))
323ad2ant2 1164 . . 3 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (𝐺𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*), ℝ*, < ))
43breq1d 4818 . 2 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐺𝐶) ≤ 𝐴 ↔ sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝐴))
5 inss2 3992 . . 3 ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*) ⊆ ℝ*
6 simp3 1168 . . 3 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → 𝐴 ∈ ℝ*)
7 supxrleub 12357 . . 3 ((((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*) ⊆ ℝ*𝐴 ∈ ℝ*) → (sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)𝑥𝐴))
85, 6, 7sylancr 581 . 2 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)𝑥𝐴))
9 imassrn 5658 . . . . . . 7 (𝐹 “ (𝐶[,)+∞)) ⊆ ran 𝐹
10 simp1r 1255 . . . . . . . 8 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → 𝐹:𝐵⟶ℝ*)
1110frnd 6229 . . . . . . 7 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ran 𝐹 ⊆ ℝ*)
129, 11syl5ss 3771 . . . . . 6 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (𝐹 “ (𝐶[,)+∞)) ⊆ ℝ*)
13 df-ss 3745 . . . . . 6 ((𝐹 “ (𝐶[,)+∞)) ⊆ ℝ* ↔ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*) = (𝐹 “ (𝐶[,)+∞)))
1412, 13sylib 209 . . . . 5 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*) = (𝐹 “ (𝐶[,)+∞)))
15 imadmres 5812 . . . . 5 (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞))) = (𝐹 “ (𝐶[,)+∞))
1614, 15syl6eqr 2816 . . . 4 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*) = (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞))))
1716raleqdv 3291 . . 3 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)𝑥𝐴 ↔ ∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥𝐴))
1810ffnd 6223 . . . 4 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → 𝐹 Fn 𝐵)
1910fdmd 6231 . . . . . . 7 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → dom 𝐹 = 𝐵)
2019ineq2d 3975 . . . . . 6 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐶[,)+∞) ∩ dom 𝐹) = ((𝐶[,)+∞) ∩ 𝐵))
21 dmres 5593 . . . . . 6 dom (𝐹 ↾ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ dom 𝐹)
22 incom 3966 . . . . . 6 (𝐵 ∩ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ 𝐵)
2320, 21, 223eqtr4g 2823 . . . . 5 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → dom (𝐹 ↾ (𝐶[,)+∞)) = (𝐵 ∩ (𝐶[,)+∞)))
24 inss1 3991 . . . . 5 (𝐵 ∩ (𝐶[,)+∞)) ⊆ 𝐵
2523, 24syl6eqss 3814 . . . 4 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → dom (𝐹 ↾ (𝐶[,)+∞)) ⊆ 𝐵)
26 breq1 4811 . . . . 5 (𝑥 = (𝐹𝑗) → (𝑥𝐴 ↔ (𝐹𝑗) ≤ 𝐴))
2726ralima 6690 . . . 4 ((𝐹 Fn 𝐵 ∧ dom (𝐹 ↾ (𝐶[,)+∞)) ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹𝑗) ≤ 𝐴))
2818, 25, 27syl2anc 579 . . 3 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹𝑗) ≤ 𝐴))
2923eleq2d 2829 . . . . . . . 8 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ 𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞))))
30 elin 3957 . . . . . . . 8 (𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞)) ↔ (𝑗𝐵𝑗 ∈ (𝐶[,)+∞)))
3129, 30syl6bb 278 . . . . . . 7 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗𝐵𝑗 ∈ (𝐶[,)+∞))))
32 simpl2 1244 . . . . . . . . 9 ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) ∧ 𝑗𝐵) → 𝐶 ∈ ℝ)
33 simp1l 1254 . . . . . . . . . 10 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → 𝐵 ⊆ ℝ)
3433sselda 3760 . . . . . . . . 9 ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) ∧ 𝑗𝐵) → 𝑗 ∈ ℝ)
35 elicopnf 12471 . . . . . . . . . 10 (𝐶 ∈ ℝ → (𝑗 ∈ (𝐶[,)+∞) ↔ (𝑗 ∈ ℝ ∧ 𝐶𝑗)))
3635baibd 535 . . . . . . . . 9 ((𝐶 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶𝑗))
3732, 34, 36syl2anc 579 . . . . . . . 8 ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) ∧ 𝑗𝐵) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶𝑗))
3837pm5.32da 574 . . . . . . 7 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝑗𝐵𝑗 ∈ (𝐶[,)+∞)) ↔ (𝑗𝐵𝐶𝑗)))
3931, 38bitrd 270 . . . . . 6 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗𝐵𝐶𝑗)))
4039imbi1d 332 . . . . 5 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) → (𝐹𝑗) ≤ 𝐴) ↔ ((𝑗𝐵𝐶𝑗) → (𝐹𝑗) ≤ 𝐴)))
41 impexp 441 . . . . 5 (((𝑗𝐵𝐶𝑗) → (𝐹𝑗) ≤ 𝐴) ↔ (𝑗𝐵 → (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴)))
4240, 41syl6bb 278 . . . 4 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) → (𝐹𝑗) ≤ 𝐴) ↔ (𝑗𝐵 → (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴))))
4342ralbidv2 3130 . . 3 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹𝑗) ≤ 𝐴 ↔ ∀𝑗𝐵 (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴)))
4417, 28, 433bitrd 296 . 2 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → (∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)𝑥𝐴 ↔ ∀𝑗𝐵 (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴)))
454, 8, 443bitrd 296 1 (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐺𝐶) ≤ 𝐴 ↔ ∀𝑗𝐵 (𝐶𝑗 → (𝐹𝑗) ≤ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3054  cin 3730  wss 3731   class class class wbr 4808  cmpt 4887  dom cdm 5276  ran crn 5277  cres 5278  cima 5279   Fn wfn 6062  wf 6063  cfv 6067  (class class class)co 6841  supcsup 8552  cr 10187  +∞cpnf 10324  *cxr 10326   < clt 10327  cle 10328  [,)cico 12378
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 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
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 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-po 5197  df-so 5198  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-sup 8554  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-ico 12382
This theorem is referenced by:  limsupgre  14498  limsupbnd1  14499  limsupbnd2  14500  mbflimsup  23723
  Copyright terms: Public domain W3C validator