Definition df-rlim 15207

Description: Define the limit relation for partial functions on the reals. See rlim 15213 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.)

Assertion

Ref	Expression
df-rlim	⊢ ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}

Distinct variable group:   𝑥,𝑤,𝑦,𝑧,𝑓

Detailed syntax breakdown of Definition df-rlim

Step	Hyp	Ref	Expression
1		crli 15203	. 2 class ⇝𝑟
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1538	. . . . . 6 class 𝑓
4		cc 10878	. . . . . . 7 class ℂ
5		cr 10879	. . . . . . 7 class ℝ
6		cpm 8625	. . . . . . 7 class ↑pm
7	4, 5, 6	co 7284	. . . . . 6 class (ℂ ↑pm ℝ)
8	3, 7	wcel 2107	. . . . 5 wff 𝑓 ∈ (ℂ ↑pm ℝ)
9		vx	. . . . . . 7 setvar 𝑥
10	9	cv 1538	. . . . . 6 class 𝑥
11	10, 4	wcel 2107	. . . . 5 wff 𝑥 ∈ ℂ
12	8, 11	wa 396	. . . 4 wff (𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ)
13		vz	. . . . . . . . . 10 setvar 𝑧
14	13	cv 1538	. . . . . . . . 9 class 𝑧
15		vw	. . . . . . . . . 10 setvar 𝑤
16	15	cv 1538	. . . . . . . . 9 class 𝑤
17		cle 11019	. . . . . . . . 9 class ≤
18	14, 16, 17	wbr 5075	. . . . . . . 8 wff 𝑧 ≤ 𝑤
19	16, 3	cfv 6437	. . . . . . . . . . 11 class (𝑓‘𝑤)
20		cmin 11214	. . . . . . . . . . 11 class −
21	19, 10, 20	co 7284	. . . . . . . . . 10 class ((𝑓‘𝑤) − 𝑥)
22		cabs 14954	. . . . . . . . . 10 class abs
23	21, 22	cfv 6437	. . . . . . . . 9 class (abs‘((𝑓‘𝑤) − 𝑥))
24		vy	. . . . . . . . . 10 setvar 𝑦
25	24	cv 1538	. . . . . . . . 9 class 𝑦
26		clt 11018	. . . . . . . . 9 class <
27	23, 25, 26	wbr 5075	. . . . . . . 8 wff (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦
28	18, 27	wi 4	. . . . . . 7 wff (𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
29	3	cdm 5590	. . . . . . 7 class dom 𝑓
30	28, 15, 29	wral 3065	. . . . . 6 wff ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
31	30, 13, 5	wrex 3066	. . . . 5 wff ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
32		crp 12739	. . . . 5 class ℝ+
33	31, 24, 32	wral 3065	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
34	12, 33	wa 396	. . 3 wff ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))
35	34, 2, 9	copab 5137	. 2 class {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}
36	1, 35	wceq 1539	1 wff ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}

This definition is referenced by:  rlimrel  15211  rlim  15213  rlimpm  15218