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

Definition df-rlim 13312
 Description: Define the limit relation for partial functions on the reals. See rlim 13318 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 13308 . 2
2 vf . . . . . . 7
32cv 1394 . . . . . 6
4 cc 9511 . . . . . . 7
5 cr 9512 . . . . . . 7
6 cpm 7440 . . . . . . 7
74, 5, 6co 6296 . . . . . 6
83, 7wcel 1818 . . . . 5
9 vx . . . . . . 7
109cv 1394 . . . . . 6
1110, 4wcel 1818 . . . . 5
128, 11wa 369 . . . 4
13 vz . . . . . . . . . 10
1413cv 1394 . . . . . . . . 9
15 vw . . . . . . . . . 10
1615cv 1394 . . . . . . . . 9
17 cle 9650 . . . . . . . . 9
1814, 16, 17wbr 4452 . . . . . . . 8
1916, 3cfv 5593 . . . . . . . . . . 11
20 cmin 9828 . . . . . . . . . . 11
2119, 10, 20co 6296 . . . . . . . . . 10
22 cabs 13067 . . . . . . . . . 10
2321, 22cfv 5593 . . . . . . . . 9
24 vy . . . . . . . . . 10
2524cv 1394 . . . . . . . . 9
26 clt 9649 . . . . . . . . 9
2723, 25, 26wbr 4452 . . . . . . . 8
2818, 27wi 4 . . . . . . 7
293cdm 5004 . . . . . . 7
3028, 15, 29wral 2807 . . . . . 6
3130, 13, 5wrex 2808 . . . . 5
32 crp 11249 . . . . 5
3331, 24, 32wral 2807 . . . 4
3412, 33wa 369 . . 3
3534, 2, 9copab 4509 . 2
361, 35wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  rlimrel  13316  rlim  13318  rlimpm  13323
 Copyright terms: Public domain W3C validator