Definition df-rlim 15656

Description: Define the limit relation for partial functions on the reals. See rlim 15662 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 15652	. 2 class ⇝𝑟
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1568	. . . . . 6 class 𝑓
4		cc 11198	. . . . . . 7 class ℂ
5		cr 11199	. . . . . . 7 class ℝ
6		cpm 8848	. . . . . . 7 class ↑pm
7	4, 5, 6	co 7420	. . . . . 6 class (ℂ ↑pm ℝ)
8	3, 7	wcel 2144	. . . . 5 wff 𝑓 ∈ (ℂ ↑pm ℝ)
9		vx	. . . . . . 7 setvar 𝑥
10	9	cv 1568	. . . . . 6 class 𝑥
11	10, 4	wcel 2144	. . . . 5 wff 𝑥 ∈ ℂ
12	8, 11	wa 401	. . . 4 wff (𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ)
13		vz	. . . . . . . . . 10 setvar 𝑧
14	13	cv 1568	. . . . . . . . 9 class 𝑧
15		vw	. . . . . . . . . 10 setvar 𝑤
16	15	cv 1568	. . . . . . . . 9 class 𝑤
17		cle 11344	. . . . . . . . 9 class ≤
18	14, 16, 17	wbr 5102	. . . . . . . 8 wff 𝑧 ≤ 𝑤
19	16, 3	cfv 6538	. . . . . . . . . . 11 class (𝑓‘𝑤)
20		cmin 11541	. . . . . . . . . . 11 class −
21	19, 10, 20	co 7420	. . . . . . . . . 10 class ((𝑓‘𝑤) − 𝑥)
22		cabs 15401	. . . . . . . . . 10 class abs
23	21, 22	cfv 6538	. . . . . . . . 9 class (abs‘((𝑓‘𝑤) − 𝑥))
24		vy	. . . . . . . . . 10 setvar 𝑦
25	24	cv 1568	. . . . . . . . 9 class 𝑦
26		clt 11343	. . . . . . . . 9 class <
27	23, 25, 26	wbr 5102	. . . . . . . 8 wff (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦
28	18, 27	wi 4	. . . . . . 7 wff (𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
29	3	cdm 5650	. . . . . . 7 class dom 𝑓
30	28, 15, 29	wral 3076	. . . . . 6 wff ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
31	30, 13, 5	wrex 3086	. . . . 5 wff ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
32		crp 13120	. . . . 5 class ℝ+
33	31, 24, 32	wral 3076	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
34	12, 33	wa 401	. . 3 wff ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))
35	34, 2, 9	copab 5166	. 2 class {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}
36	1, 35	wceq 1569	1 wff ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}

This definition is used by:  rlimrel  15660  rlim  15662  rlimpm  15667