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 20781
Description: Define a function on topologies whose value is the convergence relation for the space. Although 𝑓 is typically a function from upper integers to the topological space, it doesn't have to be. Unfortunately, the value of the function must exist to use fvmpt 6172, and we use the otherwise unnecessary conjunct dom 𝑓 ⊆ ℂ to ensure that. (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 20778 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 20455 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1473 . . . . . 6 class 𝑓
62cv 1473 . . . . . . . 8 class 𝑗
76cuni 4362 . . . . . . 7 class 𝑗
8 cc 9786 . . . . . . 7 class
9 cpm 7718 . . . . . . 7 class pm
107, 8, 9co 6523 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 1975 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1473 . . . . . 6 class 𝑥
1413, 7wcel 1975 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 1976 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1473 . . . . . . . . 9 class 𝑦
1915cv 1473 . . . . . . . . 9 class 𝑢
205, 18cres 5026 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 5782 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 11515 . . . . . . . . 9 class
2322crn 5025 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 2892 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 2891 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 1030 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4632 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4633 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1474 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  lmrel  20782  lmrcl  20783  lmfval  20784
  Copyright terms: Public domain W3C validator