Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rlim Unicode version

Definition df-rlim 11979
 Description: Define the limit relation for partial functions on the reals. See rlim 11985 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.)
Assertion
Ref Expression
df-rlim
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-rlim
StepHypRef Expression
1 crli 11975 . 2
2 vf . . . . . . 7
32cv 1631 . . . . . 6
4 cc 8751 . . . . . . 7
5 cr 8752 . . . . . . 7
6 cpm 6789 . . . . . . 7
74, 5, 6co 5874 . . . . . 6
83, 7wcel 1696 . . . . 5
9 vx . . . . . . 7
109cv 1631 . . . . . 6
1110, 4wcel 1696 . . . . 5
128, 11wa 358 . . . 4
13 vz . . . . . . . . . 10
1413cv 1631 . . . . . . . . 9
15 vw . . . . . . . . . 10
1615cv 1631 . . . . . . . . 9
17 cle 8884 . . . . . . . . 9
1814, 16, 17wbr 4039 . . . . . . . 8
1916, 3cfv 5271 . . . . . . . . . . 11
20 cmin 9053 . . . . . . . . . . 11
2119, 10, 20co 5874 . . . . . . . . . 10
22 cabs 11735 . . . . . . . . . 10
2321, 22cfv 5271 . . . . . . . . 9
24 vy . . . . . . . . . 10
2524cv 1631 . . . . . . . . 9
26 clt 8883 . . . . . . . . 9
2723, 25, 26wbr 4039 . . . . . . . 8
2818, 27wi 4 . . . . . . 7
293cdm 4705 . . . . . . 7
3028, 15, 29wral 2556 . . . . . 6
3130, 13, 5wrex 2557 . . . . 5
32 crp 10370 . . . . 5
3331, 24, 32wral 2556 . . . 4
3412, 33wa 358 . . 3
3534, 2, 9copab 4092 . 2
361, 35wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  rlimrel  11983  rlim  11985  rlimpm  11990
 Copyright terms: Public domain W3C validator