Metamath Proof Explorer

Theorem idlimc

Description: Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses idlimc.a 
|- ( ph -> A C_ CC )
idlimc.f 
|- F = ( x e. A |-> x )
idlimc.x 
|- ( ph -> X e. CC )
Assertion idlimc 
|- ( ph -> X e. ( F limCC X ) )

Proof

Step Hyp Ref Expression
1 idlimc.a 
 |-  ( ph -> A C_ CC )
2 idlimc.f 
 |-  F = ( x e. A |-> x )
3 idlimc.x 
 |-  ( ph -> X e. CC )
4 simpr 
 |-  ( ( ph /\ w e. RR+ ) -> w e. RR+ )
5 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
6 2 fvmpt2 
 |-  ( ( x e. A /\ x e. A ) -> ( F ` x ) = x )
7 5 5 6 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = x )
8 7 fvoveq1d 
 |-  ( ( ph /\ x e. A ) -> ( abs ` ( ( F ` x ) - X ) ) = ( abs ` ( x - X ) ) )
9 8 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) = ( abs ` ( x - X ) ) )
10 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( x - X ) ) < w )
11 9 10 eqbrtrd 
 |-  ( ( ( ph /\ x e. A ) /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w )
12 11 adantrl 
 |-  ( ( ( ph /\ x e. A ) /\ ( x =/= X /\ ( abs ` ( x - X ) ) < w ) ) -> ( abs ` ( ( F ` x ) - X ) ) < w )
13 12 ex 
 |-  ( ( ph /\ x e. A ) -> ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w ) )
14 13 adantlr 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. A ) -> ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w ) )
15 14 ralrimiva 
 |-  ( ( ph /\ w e. RR+ ) -> A. x e. A ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w ) )
16 nfcv 
 |-  F/_ z x
17 nfcv 
 |-  F/_ z X
18 16 17 nfne 
 |-  F/ z x =/= X
19 nfv 
 |-  F/ z ( abs ` ( x - X ) ) < w
20 18 19 nfan 
 |-  F/ z ( x =/= X /\ ( abs ` ( x - X ) ) < w )
21 nfv 
 |-  F/ z ( abs ` ( ( F ` x ) - X ) ) < w
22 20 21 nfim 
 |-  F/ z ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w )
23 nfv 
 |-  F/ x ( z =/= X /\ ( abs ` ( z - X ) ) < w )
24 nfcv 
 |-  F/_ x abs
25 nfmpt1 
 |-  F/_ x ( x e. A |-> x )
26 2 25 nfcxfr 
 |-  F/_ x F
27 nfcv 
 |-  F/_ x z
28 26 27 nffv 
 |-  F/_ x ( F ` z )
29 nfcv 
 |-  F/_ x -
30 nfcv 
 |-  F/_ x X
31 28 29 30 nfov 
 |-  F/_ x ( ( F ` z ) - X )
32 24 31 nffv 
 |-  F/_ x ( abs ` ( ( F ` z ) - X ) )
33 nfcv 
 |-  F/_ x <
34 nfcv 
 |-  F/_ x w
35 32 33 34 nfbr 
 |-  F/ x ( abs ` ( ( F ` z ) - X ) ) < w
36 23 35 nfim 
 |-  F/ x ( ( z =/= X /\ ( abs ` ( z - X ) ) < w ) -> ( abs ` ( ( F ` z ) - X ) ) < w )
37 neeq1 
 |-  ( x = z -> ( x =/= X <-> z =/= X ) )
38 fvoveq1 
 |-  ( x = z -> ( abs ` ( x - X ) ) = ( abs ` ( z - X ) ) )
39 38 breq1d 
 |-  ( x = z -> ( ( abs ` ( x - X ) ) < w <-> ( abs ` ( z - X ) ) < w ) )
40 37 39 anbi12d 
 |-  ( x = z -> ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) <-> ( z =/= X /\ ( abs ` ( z - X ) ) < w ) ) )
41 40 imbrov2fvoveq 
 |-  ( x = z -> ( ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w ) <-> ( ( z =/= X /\ ( abs ` ( z - X ) ) < w ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) ) )
42 22 36 41 cbvralw 
 |-  ( A. x e. A ( ( x =/= X /\ ( abs ` ( x - X ) ) < w ) -> ( abs ` ( ( F ` x ) - X ) ) < w ) <-> A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < w ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) )
43 15 42 sylib 
 |-  ( ( ph /\ w e. RR+ ) -> A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < w ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) )
44 brimralrspcev 
 |-  ( ( w e. RR+ /\ A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < w ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) ) -> E. y e. RR+ A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < y ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) )
45 4 43 44 syl2anc 
 |-  ( ( ph /\ w e. RR+ ) -> E. y e. RR+ A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < y ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) )
46 45 ralrimiva 
 |-  ( ph -> A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < y ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) )
47 1 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. CC )
48 47 2 fmptd 
 |-  ( ph -> F : A --> CC )
49 48 1 3 ellimc3 
 |-  ( ph -> ( X e. ( F limCC X ) <-> ( X e. CC /\ A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= X /\ ( abs ` ( z - X ) ) < y ) -> ( abs ` ( ( F ` z ) - X ) ) < w ) ) ) )
50 3 46 49 mpbir2and 
 |-  ( ph -> X e. ( F limCC X ) )