Definition df-rlim 15126

Description: Define the limit relation for partial functions on the reals. See rlim 15132 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 15122	. 2 class ⇝𝑟
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1538	. . . . . 6 class 𝑓
4		cc 10800	. . . . . . 7 class ℂ
5		cr 10801	. . . . . . 7 class ℝ
6		cpm 8574	. . . . . . 7 class ↑pm
7	4, 5, 6	co 7255	. . . . . 6 class (ℂ ↑pm ℝ)
8	3, 7	wcel 2108	. . . . 5 wff 𝑓 ∈ (ℂ ↑pm ℝ)
9		vx	. . . . . . 7 setvar 𝑥
10	9	cv 1538	. . . . . 6 class 𝑥
11	10, 4	wcel 2108	. . . . 5 wff 𝑥 ∈ ℂ
12	8, 11	wa 395	. . . 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 10941	. . . . . . . . 9 class ≤
18	14, 16, 17	wbr 5070	. . . . . . . 8 wff 𝑧 ≤ 𝑤
19	16, 3	cfv 6418	. . . . . . . . . . 11 class (𝑓‘𝑤)
20		cmin 11135	. . . . . . . . . . 11 class −
21	19, 10, 20	co 7255	. . . . . . . . . 10 class ((𝑓‘𝑤) − 𝑥)
22		cabs 14873	. . . . . . . . . 10 class abs
23	21, 22	cfv 6418	. . . . . . . . 9 class (abs‘((𝑓‘𝑤) − 𝑥))
24		vy	. . . . . . . . . 10 setvar 𝑦
25	24	cv 1538	. . . . . . . . 9 class 𝑦
26		clt 10940	. . . . . . . . 9 class <
27	23, 25, 26	wbr 5070	. . . . . . . 8 wff (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦
28	18, 27	wi 4	. . . . . . 7 wff (𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
29	3	cdm 5580	. . . . . . 7 class dom 𝑓
30	28, 15, 29	wral 3063	. . . . . 6 wff ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
31	30, 13, 5	wrex 3064	. . . . 5 wff ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
32		crp 12659	. . . . 5 class ℝ+
33	31, 24, 32	wral 3063	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦)
34	12, 33	wa 395	. . 3 wff ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))
35	34, 2, 9	copab 5132	. 2 class {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}
36	1, 35	wceq 1539	1 wff ⇝𝑟 = {⟨𝑓, 𝑥⟩ ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))}

This definition is referenced by:  rlimrel  15130  rlim  15132  rlimpm  15137