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 21014
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 6269, 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 21011 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 20679 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1480 . . . . . 6 class 𝑓
62cv 1480 . . . . . . . 8 class 𝑗
76cuni 4427 . . . . . . 7 class 𝑗
8 cc 9919 . . . . . . 7 class
9 cpm 7843 . . . . . . 7 class pm
107, 8, 9co 6635 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 1988 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1480 . . . . . 6 class 𝑥
1413, 7wcel 1988 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 1989 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1480 . . . . . . . . 9 class 𝑦
1915cv 1480 . . . . . . . . 9 class 𝑢
205, 18cres 5106 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 5872 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 11672 . . . . . . . . 9 class
2322crn 5105 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 2910 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 2909 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 1036 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4703 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4720 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1481 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  lmrel  21015  lmrcl  21016  lmfval  21017
  Copyright terms: Public domain W3C validator