Definition df-rlim 14220

Description: Define the limit relation for partial functions on the reals. See rlim 14226 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 14216	. 2 class ⇝𝑟
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1482	. . . . . 6 class 𝑓
4		cc 9934	. . . . . . 7 class ℂ
5		cr 9935	. . . . . . 7 class ℝ
6		cpm 7858	. . . . . . 7 class ↑pm
7	4, 5, 6	co 6650	. . . . . 6 class (ℂ ↑pm ℝ)
8	3, 7	wcel 1990	. . . . 5 wff 𝑓 ∈ (ℂ ↑pm ℝ)
9		vx	. . . . . . 7 setvar 𝑥
10	9	cv 1482	. . . . . 6 class 𝑥
11	10, 4	wcel 1990	. . . . 5 wff 𝑥 ∈ ℂ
12	8, 11	wa 384	. . . 4 wff (𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ)
13		vz	. . . . . . . . . 10 setvar 𝑧
14	13	cv 1482	. . . . . . . . 9 class 𝑧
15		vw	. . . . . . . . . 10 setvar 𝑤
16	15	cv 1482	. . . . . . . . 9 class 𝑤
17		cle 10075	. . . . . . . . 9 class ≤
18	14, 16, 17	wbr 4653	. . . . . . . 8 wff 𝑧 ≤ 𝑤
19	16, 3	cfv 5888	. . . . . . . . . . 11 class (𝑓‘𝑤)
20		cmin 10266	. . . . . . . . . . 11 class −
21	19, 10, 20	co 6650	. . . . . . . . . 10 class ((𝑓‘𝑤) − 𝑥)
22		cabs 13974	. . . . . . . . . 10 class abs
23	21, 22	cfv 5888	. . . . . . . . 9 class (abs‘((𝑓‘𝑤) − 𝑥))
24		vy	. . . . . . . . . 10 setvar 𝑦
25	24	cv 1482	. . . . . . . . 9 class 𝑦
26		clt 10074	. . . . . . . . 9 class <
27	23, 25, 26	wbr 4653	. . . . . . . 8 wff (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦
28	18, 27	wi 4	. . . . . . 7 wff (𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
29	3	cdm 5114	. . . . . . 7 class dom 𝑓
30	28, 15, 29	wral 2912	. . . . . 6 wff ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
31	30, 13, 5	wrex 2913	. . . . 5 wff ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
32		crp 11832	. . . . 5 class ℝ+
33	31, 24, 32	wral 2912	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
34	12, 33	wa 384	. . 3 wff ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))
35	34, 2, 9	copab 4712	. 2 class {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}
36	1, 35	wceq 1483	1 wff ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}

This definition is referenced by:  rlimrel  14224  rlim  14226  rlimpm  14231