Definition df-lm 14580

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 14577	. 2 class ⇝𝑡
2		vj	. . 3 setvar 𝑗
3		ctop 14387	. . 3 class Top
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1371	. . . . . 6 class 𝑓
6	2	cv 1371	. . . . . . . 8 class 𝑗
7	6	cuni 3849	. . . . . . 7 class ∪ 𝑗
8		cc 7905	. . . . . . 7 class ℂ
9		cpm 6726	. . . . . . 7 class ↑pm
10	7, 8, 9	co 5934	. . . . . 6 class (∪ 𝑗 ↑pm ℂ)
11	5, 10	wcel 2175	. . . . 5 wff 𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1371	. . . . . 6 class 𝑥
14	13, 7	wcel 2175	. . . . 5 wff 𝑥 ∈ ∪ 𝑗
15		vu	. . . . . . . 8 setvar 𝑢
16	12, 15	wel 2176	. . . . . . 7 wff 𝑥 ∈ 𝑢
17		vy	. . . . . . . . . 10 setvar 𝑦
18	17	cv 1371	. . . . . . . . 9 class 𝑦
19	15	cv 1371	. . . . . . . . 9 class 𝑢
20	5, 18	cres 4675	. . . . . . . . 9 class (𝑓 ↾ 𝑦)
21	18, 19, 20	wf 5264	. . . . . . . 8 wff (𝑓 ↾ 𝑦):𝑦⟶𝑢
22		cuz 9630	. . . . . . . . 9 class ℤ≥
23	22	crn 4674	. . . . . . . 8 class ran ℤ≥
24	21, 17, 23	wrex 2484	. . . . . . 7 wff ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢
25	16, 24	wi 4	. . . . . 6 wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
26	25, 15, 6	wral 2483	. . . . 5 wff ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
27	11, 14, 26	w3a 980	. . . 4 wff (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))
28	27, 4, 12	copab 4103	. . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}
29	2, 3, 28	cmpt 4104	. 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
30	1, 29	wceq 1372	1 wff ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})

This definition is referenced by:  lmrcl  14581  lmfval  14582