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

Theorem lmflf 22608
 Description: The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.)
Hypotheses
Ref Expression
lmflf.1 𝑍 = (ℤ𝑀)
lmflf.2 𝐿 = (𝑍filGen(ℤ𝑍))
Assertion
Ref Expression
lmflf ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹(⇝𝑡𝐽)𝑃𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹)))

Proof of Theorem lmflf
Dummy variables 𝑗 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzf 12234 . . . . . . . 8 :ℤ⟶𝒫 ℤ
2 ffn 6494 . . . . . . . 8 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
31, 2ax-mp 5 . . . . . . 7 Fn ℤ
4 lmflf.1 . . . . . . . 8 𝑍 = (ℤ𝑀)
5 uzssz 12252 . . . . . . . 8 (ℤ𝑀) ⊆ ℤ
64, 5eqsstri 3976 . . . . . . 7 𝑍 ⊆ ℤ
7 imaeq2 5903 . . . . . . . . 9 (𝑦 = (ℤ𝑗) → (𝐹𝑦) = (𝐹 “ (ℤ𝑗)))
87sseq1d 3973 . . . . . . . 8 (𝑦 = (ℤ𝑗) → ((𝐹𝑦) ⊆ 𝑥 ↔ (𝐹 “ (ℤ𝑗)) ⊆ 𝑥))
98rexima 6982 . . . . . . 7 ((ℤ Fn ℤ ∧ 𝑍 ⊆ ℤ) → (∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥 ↔ ∃𝑗𝑍 (𝐹 “ (ℤ𝑗)) ⊆ 𝑥))
103, 6, 9mp2an 691 . . . . . 6 (∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥 ↔ ∃𝑗𝑍 (𝐹 “ (ℤ𝑗)) ⊆ 𝑥)
11 simpl3 1190 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → 𝐹:𝑍𝑋)
1211ffund 6498 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → Fun 𝐹)
13 uzss 12253 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) → (ℤ𝑗) ⊆ (ℤ𝑀))
1413, 4eleq2s 2932 . . . . . . . . . 10 (𝑗𝑍 → (ℤ𝑗) ⊆ (ℤ𝑀))
1514adantl 485 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (ℤ𝑗) ⊆ (ℤ𝑀))
1611fdmd 6504 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → dom 𝐹 = 𝑍)
1716, 4syl6eq 2873 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → dom 𝐹 = (ℤ𝑀))
1815, 17sseqtrrd 3983 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (ℤ𝑗) ⊆ dom 𝐹)
19 funimass4 6712 . . . . . . . 8 ((Fun 𝐹 ∧ (ℤ𝑗) ⊆ dom 𝐹) → ((𝐹 “ (ℤ𝑗)) ⊆ 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥))
2012, 18, 19syl2anc 587 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → ((𝐹 “ (ℤ𝑗)) ⊆ 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥))
2120rexbidva 3282 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍 (𝐹 “ (ℤ𝑗)) ⊆ 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥))
2210, 21syl5rbb 287 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥 ↔ ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥))
2322imbi2d 344 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → ((𝑃𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥) ↔ (𝑃𝑥 → ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥)))
2423ralbidv 3187 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∀𝑥𝐽 (𝑃𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥) ↔ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥)))
2524anbi2d 631 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → ((𝑃𝑋 ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥)) ↔ (𝑃𝑋 ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥))))
26 simp1 1133 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → 𝐽 ∈ (TopOn‘𝑋))
27 simp2 1134 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → 𝑀 ∈ ℤ)
28 simp3 1135 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → 𝐹:𝑍𝑋)
29 eqidd 2823 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
3026, 4, 27, 28, 29lmbrf 21863 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝑃𝑋 ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑥))))
314uzfbas 22501 . . 3 (𝑀 ∈ ℤ → (ℤ𝑍) ∈ (fBas‘𝑍))
32 lmflf.2 . . . 4 𝐿 = (𝑍filGen(ℤ𝑍))
3332flffbas 22598 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ (ℤ𝑍) ∈ (fBas‘𝑍) ∧ 𝐹:𝑍𝑋) → (𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑃𝑋 ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥))))
3431, 33syl3an2 1161 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑃𝑋 ∧ ∀𝑥𝐽 (𝑃𝑥 → ∃𝑦 ∈ (ℤ𝑍)(𝐹𝑦) ⊆ 𝑥))))
3525, 30, 343bitr4d 314 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹(⇝𝑡𝐽)𝑃𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114  ∀wral 3130  ∃wrex 3131   ⊆ wss 3908  𝒫 cpw 4511   class class class wbr 5042  dom cdm 5532   “ cima 5535  Fun wfun 6328   Fn wfn 6329  ⟶wf 6330  ‘cfv 6334  (class class class)co 7140  ℤcz 11969  ℤ≥cuz 12231  fBascfbas 20077  filGencfg 20078  TopOnctopon 21513  ⇝𝑡clm 21829   fLimf cflf 22538 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-neg 10862  df-nn 11626  df-z 11970  df-uz 12232  df-rest 16687  df-fbas 20086  df-fg 20087  df-top 21497  df-topon 21514  df-ntr 21623  df-nei 21701  df-lm 21832  df-fil 22449  df-fm 22541  df-flim 22542  df-flf 22543 This theorem is referenced by:  cmetcaulem  23890
 Copyright terms: Public domain W3C validator