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

Theorem lmff 22557
Description: If 𝐹 converges, there is some upper integer set on which 𝐹 is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
Hypotheses
Ref Expression
lmff.1 𝑍 = (ℤ𝑀)
lmff.3 (𝜑𝐽 ∈ (TopOn‘𝑋))
lmff.4 (𝜑𝑀 ∈ ℤ)
lmff.5 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
Assertion
Ref Expression
lmff (𝜑 → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋)
Distinct variable groups:   𝑗,𝐹   𝑗,𝐽   𝑗,𝑀   𝜑,𝑗   𝑗,𝑋   𝑗,𝑍

Proof of Theorem lmff
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmff.5 . . . . . 6 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
2 eldm2g 5845 . . . . . . 7 (𝐹 ∈ dom (⇝𝑡𝐽) → (𝐹 ∈ dom (⇝𝑡𝐽) ↔ ∃𝑦𝐹, 𝑦⟩ ∈ (⇝𝑡𝐽)))
32ibi 267 . . . . . 6 (𝐹 ∈ dom (⇝𝑡𝐽) → ∃𝑦𝐹, 𝑦⟩ ∈ (⇝𝑡𝐽))
41, 3syl 17 . . . . 5 (𝜑 → ∃𝑦𝐹, 𝑦⟩ ∈ (⇝𝑡𝐽))
5 df-br 5097 . . . . . 6 (𝐹(⇝𝑡𝐽)𝑦 ↔ ⟨𝐹, 𝑦⟩ ∈ (⇝𝑡𝐽))
65exbii 1850 . . . . 5 (∃𝑦 𝐹(⇝𝑡𝐽)𝑦 ↔ ∃𝑦𝐹, 𝑦⟩ ∈ (⇝𝑡𝐽))
74, 6sylibr 233 . . . 4 (𝜑 → ∃𝑦 𝐹(⇝𝑡𝐽)𝑦)
8 lmff.3 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 lmcl 22553 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
108, 9sylan 581 . . . . 5 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
11 eleq2 2826 . . . . . . 7 (𝑗 = 𝑋 → (𝑦𝑗𝑦𝑋))
12 feq3 6638 . . . . . . . 8 (𝑗 = 𝑋 → ((𝐹𝑥):𝑥𝑗 ↔ (𝐹𝑥):𝑥𝑋))
1312rexbidv 3172 . . . . . . 7 (𝑗 = 𝑋 → (∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑗 ↔ ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋))
1411, 13imbi12d 345 . . . . . 6 (𝑗 = 𝑋 → ((𝑦𝑗 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑗) ↔ (𝑦𝑋 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋)))
158lmbr 22514 . . . . . . . 8 (𝜑 → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑗𝐽 (𝑦𝑗 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑗))))
1615biimpa 478 . . . . . . 7 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑗𝐽 (𝑦𝑗 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑗)))
1716simp3d 1144 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → ∀𝑗𝐽 (𝑦𝑗 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑗))
18 toponmax 22180 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
198, 18syl 17 . . . . . . 7 (𝜑𝑋𝐽)
2019adantr 482 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → 𝑋𝐽)
2114, 17, 20rspcdva 3574 . . . . 5 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → (𝑦𝑋 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋))
2210, 21mpd 15 . . . 4 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋)
237, 22exlimddv 1938 . . 3 (𝜑 → ∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋)
24 uzf 12690 . . . 4 :ℤ⟶𝒫 ℤ
25 ffn 6655 . . . 4 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
26 reseq2 5922 . . . . . 6 (𝑥 = (ℤ𝑗) → (𝐹𝑥) = (𝐹 ↾ (ℤ𝑗)))
27 id 22 . . . . . 6 (𝑥 = (ℤ𝑗) → 𝑥 = (ℤ𝑗))
2826, 27feq12d 6643 . . . . 5 (𝑥 = (ℤ𝑗) → ((𝐹𝑥):𝑥𝑋 ↔ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋))
2928rexrn 7023 . . . 4 (ℤ Fn ℤ → (∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋 ↔ ∃𝑗 ∈ ℤ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋))
3024, 25, 29mp2b 10 . . 3 (∃𝑥 ∈ ran ℤ(𝐹𝑥):𝑥𝑋 ↔ ∃𝑗 ∈ ℤ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋)
3123, 30sylib 217 . 2 (𝜑 → ∃𝑗 ∈ ℤ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋)
32 lmff.4 . . . 4 (𝜑𝑀 ∈ ℤ)
33 lmff.1 . . . . 5 𝑍 = (ℤ𝑀)
3433rexuz3 15159 . . . 4 (𝑀 ∈ ℤ → (∃𝑗𝑍𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋) ↔ ∃𝑗 ∈ ℤ ∀𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
3532, 34syl 17 . . 3 (𝜑 → (∃𝑗𝑍𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋) ↔ ∃𝑗 ∈ ℤ ∀𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
3616simp1d 1142 . . . . . . 7 ((𝜑𝐹(⇝𝑡𝐽)𝑦) → 𝐹 ∈ (𝑋pm ℂ))
377, 36exlimddv 1938 . . . . . 6 (𝜑𝐹 ∈ (𝑋pm ℂ))
38 pmfun 8710 . . . . . 6 (𝐹 ∈ (𝑋pm ℂ) → Fun 𝐹)
3937, 38syl 17 . . . . 5 (𝜑 → Fun 𝐹)
40 ffvresb 7058 . . . . 5 (Fun 𝐹 → ((𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋 ↔ ∀𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
4139, 40syl 17 . . . 4 (𝜑 → ((𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋 ↔ ∀𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
4241rexbidv 3172 . . 3 (𝜑 → (∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋 ↔ ∃𝑗𝑍𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
4341rexbidv 3172 . . 3 (𝜑 → (∃𝑗 ∈ ℤ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋 ↔ ∃𝑗 ∈ ℤ ∀𝑥 ∈ (ℤ𝑗)(𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ∈ 𝑋)))
4435, 42, 433bitr4d 311 . 2 (𝜑 → (∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋 ↔ ∃𝑗 ∈ ℤ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋))
4531, 44mpbird 257 1 (𝜑 → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wral 3062  wrex 3071  𝒫 cpw 4551  cop 4583   class class class wbr 5096  dom cdm 5624  ran crn 5625  cres 5626  Fun wfun 6477   Fn wfn 6478  wf 6479  cfv 6483  (class class class)co 7341  pm cpm 8691  cc 10974  cz 12424  cuz 12687  TopOnctopon 22164  𝑡clm 22482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-cnex 11032  ax-resscn 11033  ax-pre-lttri 11050  ax-pre-lttrn 11051
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-po 5536  df-so 5537  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7903  df-2nd 7904  df-er 8573  df-pm 8693  df-en 8809  df-dom 8810  df-sdom 8811  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-neg 11313  df-z 12425  df-uz 12688  df-top 22148  df-topon 22165  df-lm 22485
This theorem is referenced by:  lmle  24570
  Copyright terms: Public domain W3C validator