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 20843
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 6191, 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 20840 . 2 class 𝑡
2 vj . . 3 setvar 𝑗
3 ctop 20517 . . 3 class Top
4 vf . . . . . . 7 setvar 𝑓
54cv 1474 . . . . . 6 class 𝑓
62cv 1474 . . . . . . . 8 class 𝑗
76cuni 4372 . . . . . . 7 class 𝑗
8 cc 9813 . . . . . . 7 class
9 cpm 7745 . . . . . . 7 class pm
107, 8, 9co 6549 . . . . . 6 class ( 𝑗pm ℂ)
115, 10wcel 1977 . . . . 5 wff 𝑓 ∈ ( 𝑗pm ℂ)
12 vx . . . . . . 7 setvar 𝑥
1312cv 1474 . . . . . 6 class 𝑥
1413, 7wcel 1977 . . . . 5 wff 𝑥 𝑗
15 vu . . . . . . . 8 setvar 𝑢
1612, 15wel 1978 . . . . . . 7 wff 𝑥𝑢
17 vy . . . . . . . . . 10 setvar 𝑦
1817cv 1474 . . . . . . . . 9 class 𝑦
1915cv 1474 . . . . . . . . 9 class 𝑢
205, 18cres 5040 . . . . . . . . 9 class (𝑓𝑦)
2118, 19, 20wf 5800 . . . . . . . 8 wff (𝑓𝑦):𝑦𝑢
22 cuz 11563 . . . . . . . . 9 class
2322crn 5039 . . . . . . . 8 class ran ℤ
2421, 17, 23wrex 2897 . . . . . . 7 wff 𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢
2516, 24wi 4 . . . . . 6 wff (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2625, 15, 6wral 2896 . . . . 5 wff 𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢)
2711, 14, 26w3a 1031 . . . 4 wff (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))
2827, 4, 12copab 4642 . . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))}
292, 3, 28cmpt 4643 . 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
301, 29wceq 1475 1 wff 𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ ( 𝑗pm ℂ) ∧ 𝑥 𝑗 ∧ ∀𝑢𝑗 (𝑥𝑢 → ∃𝑦 ∈ ran ℤ(𝑓𝑦):𝑦𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  lmrel  20844  lmrcl  20845  lmfval  20846
  Copyright terms: Public domain W3C validator