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 ) )