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 ⊢⇝ℝ=fx|f∈ℂ↑𝑝𝑚ℝ∧x∈ℂ∧∀y∈ℝ+∃z∈ℝ∀w∈dom⁡fz≤w→f⁡w−x<y

Detailed syntax breakdown

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