Metamath Proof Explorer

Definition df-rlim

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

Ref Expression
Assertion df-rlim ⊢ ⇝ℝ = f x | f ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ x ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y

Detailed syntax breakdown

Step Hyp Ref Expression
0 crli class ⇝ℝ
1 vf setvar f
2 vx setvar x
3 1 cv setvar f
4 cc class ℂ
5 cpm class ↑ 𝑝𝑚
6 cr class ℝ
7 4 6 5 co class ℂ ↑ 𝑝𝑚 ℝ
8 3 7 wcel wff f ∈ ℂ ↑ 𝑝𝑚 ℝ
9 2 cv setvar x
10 9 4 wcel wff x ∈ ℂ
11 8 10 wa wff f ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ x ∈ ℂ
12 vy setvar y
13 crp class ℝ +
14 vz setvar z
15 vw setvar w
16 3 cdm class dom ⁡ f
17 14 cv setvar z
18 cle class ≤
19 15 cv setvar w
20 17 19 18 wbr wff z ≤ w
21 cabs class abs
22 19 3 cfv class f ⁡ w
23 cmin class −
24 22 9 23 co class f ⁡ w − x
25 24 21 cfv class f ⁡ w − x
26 clt class <
27 12 cv setvar y
28 25 27 26 wbr wff f ⁡ w − x < y
29 20 28 wi wff z ≤ w → f ⁡ w − x < y
30 29 15 16 wral wff ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y
31 30 14 6 wrex wff ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y
32 31 12 13 wral wff ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y
33 11 32 wa wff f ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ x ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y
34 33 1 2 copab class f x | f ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ x ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y
35 0 34 wceq wff ⇝ℝ = f x | f ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ x ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ w ∈ dom ⁡ f z ≤ w → f ⁡ w − x < y