Definition df-lm 22725

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

Step	Hyp	Ref	Expression
1		clm 22722	. 2 class ⇝𝑡
2		vj	. . 3 setvar 𝑗
3		ctop 22387	. . 3 class Top
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1541	. . . . . 6 class 𝑓
6	2	cv 1541	. . . . . . . 8 class 𝑗
7	6	cuni 4908	. . . . . . 7 class ∪ 𝑗
8		cc 11105	. . . . . . 7 class ℂ
9		cpm 8818	. . . . . . 7 class ↑pm
10	7, 8, 9	co 7406	. . . . . 6 class (∪ 𝑗 ↑pm ℂ)
11	5, 10	wcel 2107	. . . . 5 wff 𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1541	. . . . . 6 class 𝑥
14	13, 7	wcel 2107	. . . . 5 wff 𝑥 ∈ ∪ 𝑗
15		vu	. . . . . . . 8 setvar 𝑢
16	12, 15	wel 2108	. . . . . . 7 wff 𝑥 ∈ 𝑢
17		vy	. . . . . . . . . 10 setvar 𝑦
18	17	cv 1541	. . . . . . . . 9 class 𝑦
19	15	cv 1541	. . . . . . . . 9 class 𝑢
20	5, 18	cres 5678	. . . . . . . . 9 class (𝑓 ↾ 𝑦)
21	18, 19, 20	wf 6537	. . . . . . . 8 wff (𝑓 ↾ 𝑦):𝑦⟶𝑢
22		cuz 12819	. . . . . . . . 9 class ℤ≥
23	22	crn 5677	. . . . . . . 8 class ran ℤ≥
24	21, 17, 23	wrex 3071	. . . . . . 7 wff ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢
25	16, 24	wi 4	. . . . . 6 wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
26	25, 15, 6	wral 3062	. . . . 5 wff ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
27	11, 14, 26	w3a 1088	. . . 4 wff (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))
28	27, 4, 12	copab 5210	. . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}
29	2, 3, 28	cmpt 5231	. 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
30	1, 29	wceq 1542	1 wff ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})

This definition is referenced by:  lmrel  22726  lmrcl  22727  lmfval  22728