Definition df-lm 14879

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 14876	. 2 class ⇝𝑡
2		vj	. . 3 setvar 𝑗
3		ctop 14686	. . 3 class Top
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1394	. . . . . 6 class 𝑓
6	2	cv 1394	. . . . . . . 8 class 𝑗
7	6	cuni 3888	. . . . . . 7 class ∪ 𝑗
8		cc 8008	. . . . . . 7 class ℂ
9		cpm 6804	. . . . . . 7 class ↑pm
10	7, 8, 9	co 6007	. . . . . 6 class (∪ 𝑗 ↑pm ℂ)
11	5, 10	wcel 2200	. . . . 5 wff 𝑓 ∈ (∪ 𝑗 ↑pm ℂ)
12		vx	. . . . . . 7 setvar 𝑥
13	12	cv 1394	. . . . . 6 class 𝑥
14	13, 7	wcel 2200	. . . . 5 wff 𝑥 ∈ ∪ 𝑗
15		vu	. . . . . . . 8 setvar 𝑢
16	12, 15	wel 2201	. . . . . . 7 wff 𝑥 ∈ 𝑢
17		vy	. . . . . . . . . 10 setvar 𝑦
18	17	cv 1394	. . . . . . . . 9 class 𝑦
19	15	cv 1394	. . . . . . . . 9 class 𝑢
20	5, 18	cres 4721	. . . . . . . . 9 class (𝑓 ↾ 𝑦)
21	18, 19, 20	wf 5314	. . . . . . . 8 wff (𝑓 ↾ 𝑦):𝑦⟶𝑢
22		cuz 9733	. . . . . . . . 9 class ℤ≥
23	22	crn 4720	. . . . . . . 8 class ran ℤ≥
24	21, 17, 23	wrex 2509	. . . . . . 7 wff ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢
25	16, 24	wi 4	. . . . . 6 wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
26	25, 15, 6	wral 2508	. . . . 5 wff ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)
27	11, 14, 26	w3a 1002	. . . 4 wff (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))
28	27, 4, 12	copab 4144	. . 3 class {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}
29	2, 3, 28	cmpt 4145	. 2 class (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
30	1, 29	wceq 1395	1 wff ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})

This definition is referenced by:  lmrel  14880  lmrcl  14881  lmfval  14882