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

Definition df-lm 21241
Description: Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although 𝑓 is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function (𝑥 ∈ ℝ ↦ (sin‘(π · 𝑥))) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
Assertion
Ref Expression
df-lm 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Distinct variable group:   𝑓,𝑗,𝑥,𝑦,𝑢

Detailed syntax breakdown of Definition df-lm
StepHypRef Expression
1 clm 21238 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 20905 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1636 . . . . . 6 class 𝑓
62cv 1636 . . . . . . . 8 class 𝑗
76cuni 4623 . . . . . . 7 class 𝑗
8 cc 10213 . . . . . . 7 class
9 cpm 8087 . . . . . . 7 class pm
107, 8, 9co 6868 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 2155 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1636 . . . . . 6 class 𝑥
1413, 7wcel 2155 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 2156 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1636 . . . . . . . . 9 class 𝑦
1915cv 1636 . . . . . . . . 9 class 𝑢
205, 18cres 5307 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 6091 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 11898 . . . . . . . . 9 class
2322crn 5306 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 3093 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 3092 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 1100 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4899 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4916 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1637 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  lmrel  21242  lmrcl  21243  lmfval  21244
  Copyright terms: Public domain W3C validator