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

Theorem lmfval 22383
Description: The relation "sequence 𝑓 converges to point 𝑦 " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
lmfval (𝐽 ∈ (TopOn‘𝑋) → (⇝𝑡𝐽) = {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Distinct variable groups:   𝑥,𝑓,𝑦,𝑋   𝑢,𝑓,𝐽,𝑥,𝑦
Allowed substitution hint:   𝑋(𝑢)

Proof of Theorem lmfval
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 df-lm 22380 . 2 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
2 simpr 485 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
32unieqd 4853 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
4 toponuni 22063 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
54adantr 481 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑋 = 𝐽)
63, 5eqtr4d 2781 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → 𝑗 = 𝑋)
76oveq1d 7290 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ( 𝑗pm ℂ) = (𝑋pm ℂ))
87eleq2d 2824 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (𝑓 ∈ ( 𝑗pm ℂ) ↔ 𝑓 ∈ (𝑋pm ℂ)))
96eleq2d 2824 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (𝑥 𝑗𝑥𝑋))
102raleqdv 3348 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → (∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢) ↔ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)))
118, 9, 103anbi123d 1435 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → ((𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)) ↔ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))))
1211opabbidv 5140 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑗 = 𝐽) → {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} = {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
13 topontop 22062 . 2 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
14 df-3an 1088 . . . . 5 ((𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)) ↔ ((𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋) ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)))
1514opabbii 5141 . . . 4 {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋) ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
16 opabssxp 5679 . . . 4 {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋) ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} ⊆ ((𝑋pm ℂ) × 𝑋)
1715, 16eqsstri 3955 . . 3 {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} ⊆ ((𝑋pm ℂ) × 𝑋)
18 ovex 7308 . . . 4 (𝑋pm ℂ) ∈ V
19 toponmax 22075 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
20 xpexg 7600 . . . 4 (((𝑋pm ℂ) ∈ V ∧ 𝑋𝐽) → ((𝑋pm ℂ) × 𝑋) ∈ V)
2118, 19, 20sylancr 587 . . 3 (𝐽 ∈ (TopOn‘𝑋) → ((𝑋pm ℂ) × 𝑋) ∈ V)
22 ssexg 5247 . . 3 (({⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} ⊆ ((𝑋pm ℂ) × 𝑋) ∧ ((𝑋pm ℂ) × 𝑋) ∈ V) → {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} ∈ V)
2317, 21, 22sylancr 587 . 2 (𝐽 ∈ (TopOn‘𝑋) → {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))} ∈ V)
241, 12, 13, 23fvmptd2 6883 1 (𝐽 ∈ (TopOn‘𝑋) → (⇝𝑡𝐽) = {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋pm ℂ) ∧ 𝑥𝑋 ∧ ∀𝑢𝐽 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1539  wcel 2106  wral 3064  wrex 3065  Vcvv 3432  wss 3887   cuni 4839  {copab 5136   × cxp 5587  ran crn 5590  cres 5591  wf 6429  cfv 6433  (class class class)co 7275  pm cpm 8616  cc 10869  cuz 12582  Topctop 22042  TopOnctopon 22059  𝑡clm 22377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-top 22043  df-topon 22060  df-lm 22380
This theorem is referenced by:  lmbr  22409  sslm  22450
  Copyright terms: Public domain W3C validator