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

Definition df-rlim 12288
 Description: Define the limit relation for partial functions on the reals. See rlim 12294 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 12284 . 2
2 vf . . . . . . 7
32cv 1652 . . . . . 6
4 cc 8993 . . . . . . 7
5 cr 8994 . . . . . . 7
6 cpm 7022 . . . . . . 7
74, 5, 6co 6084 . . . . . 6
83, 7wcel 1726 . . . . 5
9 vx . . . . . . 7
109cv 1652 . . . . . 6
1110, 4wcel 1726 . . . . 5
128, 11wa 360 . . . 4
13 vz . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
15 vw . . . . . . . . . 10
1615cv 1652 . . . . . . . . 9
17 cle 9126 . . . . . . . . 9
1814, 16, 17wbr 4215 . . . . . . . 8
1916, 3cfv 5457 . . . . . . . . . . 11
20 cmin 9296 . . . . . . . . . . 11
2119, 10, 20co 6084 . . . . . . . . . 10
22 cabs 12044 . . . . . . . . . 10
2321, 22cfv 5457 . . . . . . . . 9
24 vy . . . . . . . . . 10
2524cv 1652 . . . . . . . . 9
26 clt 9125 . . . . . . . . 9
2723, 25, 26wbr 4215 . . . . . . . 8
2818, 27wi 4 . . . . . . 7
293cdm 4881 . . . . . . 7
3028, 15, 29wral 2707 . . . . . 6
3130, 13, 5wrex 2708 . . . . 5
32 crp 10617 . . . . 5
3331, 24, 32wral 2707 . . . 4
3412, 33wa 360 . . 3
3534, 2, 9copab 4268 . 2
361, 35wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  rlimrel  12292  rlim  12294  rlimpm  12299
 Copyright terms: Public domain W3C validator