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 
|- ~~>r = { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crli 
 |-  ~~>r
1 vf 
 |-  f
2 vx 
 |-  x
3 1 cv 
 |-  f
4 cc 
 |-  CC
5 cpm 
 |-  ^pm
6 cr 
 |-  RR
7 4 6 5 co 
 |-  ( CC ^pm RR )
8 3 7 wcel 
 |-  f e. ( CC ^pm RR )
9 2 cv 
 |-  x
10 9 4 wcel 
 |-  x e. CC
11 8 10 wa 
 |-  ( f e. ( CC ^pm RR ) /\ x e. CC )
12 vy 
 |-  y
13 crp 
 |-  RR+
14 vz 
 |-  z
15 vw 
 |-  w
16 3 cdm 
 |-  dom f
17 14 cv 
 |-  z
18 cle 
 |-  <_
19 15 cv 
 |-  w
20 17 19 18 wbr 
 |-  z <_ w
21 cabs 
 |-  abs
22 19 3 cfv 
 |-  ( f ` w )
23 cmin 
 |-  -
24 22 9 23 co 
 |-  ( ( f ` w ) - x )
25 24 21 cfv 
 |-  ( abs ` ( ( f ` w ) - x ) )
26 clt 
 |-  <
27 12 cv 
 |-  y
28 25 27 26 wbr 
 |-  ( abs ` ( ( f ` w ) - x ) ) < y
29 20 28 wi 
 |-  ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y )
30 29 15 16 wral 
 |-  A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y )
31 30 14 6 wrex 
 |-  E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y )
32 31 12 13 wral 
 |-  A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y )
33 11 32 wa 
 |-  ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) )
34 33 1 2 copab 
 |-  { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }
35 0 34 wceq 
 |-  ~~>r = { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }