This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limcdif

Description: It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis limccl.f 
|- ( ph -> F : A --> CC )
Assertion limcdif 
|- ( ph -> ( F limCC B ) = ( ( F |` ( A \ { B } ) ) limCC B ) )

Proof

Step Hyp Ref Expression
1 limccl.f 
 |-  ( ph -> F : A --> CC )
2 1 fdmd 
 |-  ( ph -> dom F = A )
3 2 adantr 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> dom F = A )
4 limcrcl 
 |-  ( x e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
5 4 adantl 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
6 5 simp2d 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> dom F C_ CC )
7 3 6 eqsstrrd 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> A C_ CC )
8 5 simp3d 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> B e. CC )
9 7 8 jca 
 |-  ( ( ph /\ x e. ( F limCC B ) ) -> ( A C_ CC /\ B e. CC ) )
10 9 ex 
 |-  ( ph -> ( x e. ( F limCC B ) -> ( A C_ CC /\ B e. CC ) ) )
11 undif1 
 |-  ( ( A \ { B } ) u. { B } ) = ( A u. { B } )
12 difss 
 |-  ( A \ { B } ) C_ A
13 fssres 
 |-  ( ( F : A --> CC /\ ( A \ { B } ) C_ A ) -> ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC )
14 1 12 13 sylancl 
 |-  ( ph -> ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC )
15 14 fdmd 
 |-  ( ph -> dom ( F |` ( A \ { B } ) ) = ( A \ { B } ) )
16 15 adantr 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> dom ( F |` ( A \ { B } ) ) = ( A \ { B } ) )
17 limcrcl 
 |-  ( x e. ( ( F |` ( A \ { B } ) ) limCC B ) -> ( ( F |` ( A \ { B } ) ) : dom ( F |` ( A \ { B } ) ) --> CC /\ dom ( F |` ( A \ { B } ) ) C_ CC /\ B e. CC ) )
18 17 adantl 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> ( ( F |` ( A \ { B } ) ) : dom ( F |` ( A \ { B } ) ) --> CC /\ dom ( F |` ( A \ { B } ) ) C_ CC /\ B e. CC ) )
19 18 simp2d 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> dom ( F |` ( A \ { B } ) ) C_ CC )
20 16 19 eqsstrrd 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> ( A \ { B } ) C_ CC )
21 18 simp3d 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> B e. CC )
22 21 snssd 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> { B } C_ CC )
23 20 22 unssd 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> ( ( A \ { B } ) u. { B } ) C_ CC )
24 11 23 eqsstrrid 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> ( A u. { B } ) C_ CC )
25 24 unssad 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> A C_ CC )
26 25 21 jca 
 |-  ( ( ph /\ x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) -> ( A C_ CC /\ B e. CC ) )
27 26 ex 
 |-  ( ph -> ( x e. ( ( F |` ( A \ { B } ) ) limCC B ) -> ( A C_ CC /\ B e. CC ) ) )
28 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( A u. { B } ) )
29 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
30 eqid 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) )
31 1 adantr 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> F : A --> CC )
32 simprl 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> A C_ CC )
33 simprr 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> B e. CC )
34 28 29 30 31 32 33 ellimc 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> ( x e. ( F limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A u. { B } ) ) CnP ( TopOpen ` CCfld ) ) ` B ) ) )
35 11 eqcomi 
 |-  ( A u. { B } ) = ( ( A \ { B } ) u. { B } )
36 35 oveq2i 
 |-  ( ( TopOpen ` CCfld ) |`t ( A u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A \ { B } ) u. { B } ) )
37 35 mpteq1i 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) = ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , x , ( F ` z ) ) )
38 elun 
 |-  ( z e. ( ( A \ { B } ) u. { B } ) <-> ( z e. ( A \ { B } ) \/ z e. { B } ) )
39 velsn 
 |-  ( z e. { B } <-> z = B )
40 39 orbi2i 
 |-  ( ( z e. ( A \ { B } ) \/ z e. { B } ) <-> ( z e. ( A \ { B } ) \/ z = B ) )
41 pm5.61 
 |-  ( ( ( z e. ( A \ { B } ) \/ z = B ) /\ -. z = B ) <-> ( z e. ( A \ { B } ) /\ -. z = B ) )
42 fvres 
 |-  ( z e. ( A \ { B } ) -> ( ( F |` ( A \ { B } ) ) ` z ) = ( F ` z ) )
43 42 adantr 
 |-  ( ( z e. ( A \ { B } ) /\ -. z = B ) -> ( ( F |` ( A \ { B } ) ) ` z ) = ( F ` z ) )
44 41 43 sylbi 
 |-  ( ( ( z e. ( A \ { B } ) \/ z = B ) /\ -. z = B ) -> ( ( F |` ( A \ { B } ) ) ` z ) = ( F ` z ) )
45 44 ifeq2da 
 |-  ( ( z e. ( A \ { B } ) \/ z = B ) -> if ( z = B , x , ( ( F |` ( A \ { B } ) ) ` z ) ) = if ( z = B , x , ( F ` z ) ) )
46 40 45 sylbi 
 |-  ( ( z e. ( A \ { B } ) \/ z e. { B } ) -> if ( z = B , x , ( ( F |` ( A \ { B } ) ) ` z ) ) = if ( z = B , x , ( F ` z ) ) )
47 38 46 sylbi 
 |-  ( z e. ( ( A \ { B } ) u. { B } ) -> if ( z = B , x , ( ( F |` ( A \ { B } ) ) ` z ) ) = if ( z = B , x , ( F ` z ) ) )
48 47 mpteq2ia 
 |-  ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , x , ( ( F |` ( A \ { B } ) ) ` z ) ) ) = ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , x , ( F ` z ) ) )
49 37 48 eqtr4i 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) = ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , x , ( ( F |` ( A \ { B } ) ) ` z ) ) )
50 14 adantr 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC )
51 32 ssdifssd 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> ( A \ { B } ) C_ CC )
52 36 29 49 50 51 33 ellimc 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> ( x e. ( ( F |` ( A \ { B } ) ) limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , x , ( F ` z ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A u. { B } ) ) CnP ( TopOpen ` CCfld ) ) ` B ) ) )
53 34 52 bitr4d 
 |-  ( ( ph /\ ( A C_ CC /\ B e. CC ) ) -> ( x e. ( F limCC B ) <-> x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) )
54 53 ex 
 |-  ( ph -> ( ( A C_ CC /\ B e. CC ) -> ( x e. ( F limCC B ) <-> x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) ) )
55 10 27 54 pm5.21ndd 
 |-  ( ph -> ( x e. ( F limCC B ) <-> x e. ( ( F |` ( A \ { B } ) ) limCC B ) ) )
56 55 eqrdv 
 |-  ( ph -> ( F limCC B ) = ( ( F |` ( A \ { B } ) ) limCC B ) )