Definition df-lm 23386

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 23383	. 2 class ⇝𝑡
2		vj	. . 3 setvar 𝑗
3		ctop 23050	. . 3 class Top
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1569	. . . . . 6 class 𝑓
6	2	cv 1569	. . . . . . . 8 class 𝑗
7	6	cuni 4872	. . . . . . 7 class ∪ 𝑗
8		cc 11093	. . . . . . 7 class ℂ
9		cpm 8821	. . . . . . 7 class ↑pm
10	7, 8, 9	co 7410	. . . . . 6 class (∪ 𝑗 ↑pm ℂ)
11	5, 10	wcel 2143	. . . . 5 wff 𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1569	. . . . . 6 class 𝑥
14	13, 7	wcel 2143	. . . . 5 wff 𝑥 ∈ ∪ 𝑗
15		vu	. . . . . . . 8 setvar 𝑢
16	12, 15	wel 2144	. . . . . . 7 wff 𝑥 ∈ 𝑢
17		vy	. . . . . . . . . 10 setvar 𝑦
18	17	cv 1569	. . . . . . . . 9 class 𝑦
19	15	cv 1569	. . . . . . . . 9 class 𝑢
20	5, 18	cres 5663	. . . . . . . . 9 class (𝑓 ↾ 𝑦)
21	18, 19, 20	wf 6532	. . . . . . . 8 wff (𝑓 ↾ 𝑦):𝑦⟶𝑢
22		cuz 12857	. . . . . . . . 9 class ℤ≥
23	22	crn 5662	. . . . . . . 8 class ran ℤ≥
24	21, 17, 23	wrex 3089	. . . . . . 7 wff ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢
25	16, 24	wi 4	. . . . . 6 wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
26	25, 15, 6	wral 3079	. . . . 5 wff ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
27	11, 14, 26	w3a 1103	. . . 4 wff (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))
28	27, 4, 12	copab 5173	. . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}
29	2, 3, 28	cmpt 5192	. 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
30	1, 29	wceq 1570	1 wff ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})

This definition is referenced by:  lmrel  23387  lmrcl  23388  lmfval  23389