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 21081
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 21078 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 20746 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1522 . . . . . 6 class 𝑓
62cv 1522 . . . . . . . 8 class 𝑗
76cuni 4468 . . . . . . 7 class 𝑗
8 cc 9972 . . . . . . 7 class
9 cpm 7900 . . . . . . 7 class pm
107, 8, 9co 6690 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 2030 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1522 . . . . . 6 class 𝑥
1413, 7wcel 2030 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 2031 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1522 . . . . . . . . 9 class 𝑦
1915cv 1522 . . . . . . . . 9 class 𝑢
205, 18cres 5145 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 5922 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 11725 . . . . . . . . 9 class
2322crn 5144 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 2942 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 2941 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 1054 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4745 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4762 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1523 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  lmrel  21082  lmrcl  21083  lmfval  21084
  Copyright terms: Public domain W3C validator