Definition df-lm 14150

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 14147	. 2 class ⇝𝑡
2		vj	. . 3 setvar 𝑗
3		ctop 13957	. . 3 class Top
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1363	. . . . . 6 class 𝑓
6	2	cv 1363	. . . . . . . 8 class 𝑗
7	6	cuni 3824	. . . . . . 7 class ∪ 𝑗
8		cc 7839	. . . . . . 7 class ℂ
9		cpm 6675	. . . . . . 7 class ↑pm
10	7, 8, 9	co 5896	. . . . . 6 class (∪ 𝑗 ↑pm ℂ)
11	5, 10	wcel 2160	. . . . 5 wff 𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1363	. . . . . 6 class 𝑥
14	13, 7	wcel 2160	. . . . 5 wff 𝑥 ∈ ∪ 𝑗
15		vu	. . . . . . . 8 setvar 𝑢
16	12, 15	wel 2161	. . . . . . 7 wff 𝑥 ∈ 𝑢
17		vy	. . . . . . . . . 10 setvar 𝑦
18	17	cv 1363	. . . . . . . . 9 class 𝑦
19	15	cv 1363	. . . . . . . . 9 class 𝑢
20	5, 18	cres 4646	. . . . . . . . 9 class (𝑓 ↾ 𝑦)
21	18, 19, 20	wf 5231	. . . . . . . 8 wff (𝑓 ↾ 𝑦):𝑦⟶𝑢
22		cuz 9558	. . . . . . . . 9 class ℤ≥
23	22	crn 4645	. . . . . . . 8 class ran ℤ≥
24	21, 17, 23	wrex 2469	. . . . . . 7 wff ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢
25	16, 24	wi 4	. . . . . 6 wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
26	25, 15, 6	wral 2468	. . . . 5 wff ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
27	11, 14, 26	w3a 980	. . . 4 wff (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))
28	27, 4, 12	copab 4078	. . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}
29	2, 3, 28	cmpt 4079	. 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
30	1, 29	wceq 1364	1 wff ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})

This definition is referenced by:  lmrcl  14151  lmfval  14152