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

Theorem xlimmnfvlem1 41523
Description: Lemma for xlimmnfv 41525: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
Hypotheses
Ref Expression
xlimmnfvlem1.m (𝜑𝑀 ∈ ℤ)
xlimmnfvlem1.z 𝑍 = (ℤ𝑀)
xlimmnfvlem1.f (𝜑𝐹:𝑍⟶ℝ*)
xlimmnfvlem1.c (𝜑𝐹~~>*-∞)
xlimmnfvlem1.x (𝜑𝑋 ∈ ℝ)
Assertion
Ref Expression
xlimmnfvlem1 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋)
Distinct variable groups:   𝑗,𝐹,𝑘   𝑗,𝑀   𝑗,𝑋,𝑘   𝑗,𝑍,𝑘   𝜑,𝑗,𝑘
Allowed substitution hint:   𝑀(𝑘)

Proof of Theorem xlimmnfvlem1
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 icomnfordt 21522 . . . . . 6 (-∞[,)𝑋) ∈ (ordTop‘ ≤ )
21a1i 11 . . . . 5 (𝜑 → (-∞[,)𝑋) ∈ (ordTop‘ ≤ ))
3 xlimmnfvlem1.c . . . . . . . 8 (𝜑𝐹~~>*-∞)
4 df-xlim 41510 . . . . . . . . 9 ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
54breqi 4933 . . . . . . . 8 (𝐹~~>*-∞ ↔ 𝐹(⇝𝑡‘(ordTop‘ ≤ ))-∞)
63, 5sylib 210 . . . . . . 7 (𝜑𝐹(⇝𝑡‘(ordTop‘ ≤ ))-∞)
7 nfcv 2929 . . . . . . . 8 𝑘𝐹
8 letopon 21511 . . . . . . . . 9 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
98a1i 11 . . . . . . . 8 (𝜑 → (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*))
107, 9lmbr3 41438 . . . . . . 7 (𝜑 → (𝐹(⇝𝑡‘(ordTop‘ ≤ ))-∞ ↔ (𝐹 ∈ (ℝ*pm ℂ) ∧ -∞ ∈ ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢)))))
116, 10mpbid 224 . . . . . 6 (𝜑 → (𝐹 ∈ (ℝ*pm ℂ) ∧ -∞ ∈ ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢))))
1211simp3d 1124 . . . . 5 (𝜑 → ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢)))
132, 12jca 504 . . . 4 (𝜑 → ((-∞[,)𝑋) ∈ (ordTop‘ ≤ ) ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢))))
1411simp2d 1123 . . . . 5 (𝜑 → -∞ ∈ ℝ*)
15 xlimmnfvlem1.x . . . . . 6 (𝜑𝑋 ∈ ℝ)
1615rexrd 10486 . . . . 5 (𝜑𝑋 ∈ ℝ*)
1715mnfltd 12333 . . . . 5 (𝜑 → -∞ < 𝑋)
18 lbico1 12604 . . . . 5 ((-∞ ∈ ℝ*𝑋 ∈ ℝ* ∧ -∞ < 𝑋) → -∞ ∈ (-∞[,)𝑋))
1914, 16, 17, 18syl3anc 1351 . . . 4 (𝜑 → -∞ ∈ (-∞[,)𝑋))
20 eleq2 2851 . . . . . 6 (𝑢 = (-∞[,)𝑋) → (-∞ ∈ 𝑢 ↔ -∞ ∈ (-∞[,)𝑋)))
21 eleq2 2851 . . . . . . . . 9 (𝑢 = (-∞[,)𝑋) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (-∞[,)𝑋)))
2221anbi2d 619 . . . . . . . 8 (𝑢 = (-∞[,)𝑋) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢) ↔ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))))
2322ralbidv 3144 . . . . . . 7 (𝑢 = (-∞[,)𝑋) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢) ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))))
2423rexbidv 3239 . . . . . 6 (𝑢 = (-∞[,)𝑋) → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))))
2520, 24imbi12d 337 . . . . 5 (𝑢 = (-∞[,)𝑋) → ((-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢)) ↔ (-∞ ∈ (-∞[,)𝑋) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)))))
2625rspcva 3530 . . . 4 (((-∞[,)𝑋) ∈ (ordTop‘ ≤ ) ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑢))) → (-∞ ∈ (-∞[,)𝑋) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))))
2713, 19, 26sylc 65 . . 3 (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)))
28 nfv 1873 . . . 4 𝑗𝜑
29 nfv 1873 . . . . . 6 𝑘𝜑
30 xlimmnfvlem1.f . . . . . . . . . . . 12 (𝜑𝐹:𝑍⟶ℝ*)
3130ffdmd 6364 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℝ*)
3231ffvelrnda 6674 . . . . . . . . . 10 ((𝜑𝑘 ∈ dom 𝐹) → (𝐹𝑘) ∈ ℝ*)
3332adantrr 704 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → (𝐹𝑘) ∈ ℝ*)
3416adantr 473 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → 𝑋 ∈ ℝ*)
3514adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → -∞ ∈ ℝ*)
36 simprr 760 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → (𝐹𝑘) ∈ (-∞[,)𝑋))
3735, 34, 36icoltubd 41231 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → (𝐹𝑘) < 𝑋)
3833, 34, 37xrltled 12357 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋))) → (𝐹𝑘) ≤ 𝑋)
3938ex 405 . . . . . . 7 (𝜑 → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)) → (𝐹𝑘) ≤ 𝑋))
4039adantr 473 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)) → (𝐹𝑘) ≤ 𝑋))
4129, 40ralimda 40807 . . . . 5 (𝜑 → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋))
4241a1d 25 . . . 4 (𝜑 → (𝑗 ∈ ℤ → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋)))
4328, 42reximdai 3251 . . 3 (𝜑 → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ (-∞[,)𝑋)) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋))
4427, 43mpd 15 . 2 (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋)
45 xlimmnfvlem1.m . . 3 (𝜑𝑀 ∈ ℤ)
46 xlimmnfvlem1.z . . . 4 𝑍 = (ℤ𝑀)
4746rexuz3 14563 . . 3 (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋))
4845, 47syl 17 . 2 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋))
4944, 48mpbird 249 1 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ≤ 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2048  wral 3085  wrex 3086   class class class wbr 4927  dom cdm 5404  wf 6182  cfv 6186  (class class class)co 6974  pm cpm 8203  cc 10329  cr 10330  -∞cmnf 10468  *cxr 10469   < clt 10470  cle 10471  cz 11790  cuz 12055  [,)cico 12553  ordTopcordt 16622  TopOnctopon 21216  𝑡clm 21532  ~~>*clsxlim 41509
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
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-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-int 4748  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  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-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  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-om 7395  df-1st 7498  df-2nd 7499  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-1o 7901  df-oadd 7905  df-er 8085  df-pm 8205  df-en 8303  df-dom 8304  df-sdom 8305  df-fin 8306  df-fi 8666  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-z 11791  df-uz 12056  df-ioo 12555  df-ioc 12556  df-ico 12557  df-icc 12558  df-topgen 16567  df-ordt 16624  df-ps 17662  df-tsr 17663  df-top 21200  df-topon 21217  df-bases 21252  df-lm 21535  df-xlim 41510
This theorem is referenced by:  xlimmnfv  41525
  Copyright terms: Public domain W3C validator