Theorem ellimc

Description: Value of the limit predicate. C is the limit of the function F at B if the function G , formed by adding B to the domain of F and setting it to C , is continuous at B . (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	limcval.j	|- J = ( K |`t ( A u. { B } ) )
	limcval.k	|- K = ( TopOpen ` CCfld )
	ellimc.g	|- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )
	ellimc.f	|- ( ph -> F : A --> CC )
	ellimc.a	|- ( ph -> A C_ CC )
	ellimc.b	|- ( ph -> B e. CC )
Assertion	ellimc	|- ( ph -> ( C e. ( F limCC B ) <-> G e. ( ( J CnP K ) ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		limcval.j	|- J = ( K |`t ( A u. { B } ) )
2		limcval.k	|- K = ( TopOpen ` CCfld )
3		ellimc.g	|- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )
4		ellimc.f	|- ( ph -> F : A --> CC )
5		ellimc.a	|- ( ph -> A C_ CC )
6		ellimc.b	|- ( ph -> B e. CC )
7	1 2	limcfval	|- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F limCC B ) C_ CC ) )
8	4 5 6 7	syl3anc	|- ( ph -> ( ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F limCC B ) C_ CC ) )
9	8	simpld	|- ( ph -> ( F limCC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } )
10	9	eleq2d	|- ( ph -> ( C e. ( F limCC B ) <-> C e. { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } ) )
11	1 2 3	limcvallem	|- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) )
12	4 5 6 11	syl3anc	|- ( ph -> ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) )
13		ifeq1	|- ( y = C -> if ( z = B , y , ( F ` z ) ) = if ( z = B , C , ( F ` z ) ) )
14	13	mpteq2dv	|- ( y = C -> ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) ) )
15	14 3	eqtr4di	|- ( y = C -> ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) = G )
16	15	eleq1d	|- ( y = C -> ( ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) <-> G e. ( ( J CnP K ) ` B ) ) )
17	16	elab3g	|- ( ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) -> ( C e. { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } <-> G e. ( ( J CnP K ) ` B ) ) )
18	12 17	syl	|- ( ph -> ( C e. { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } <-> G e. ( ( J CnP K ) ` B ) ) )
19	10 18	bitrd	|- ( ph -> ( C e. ( F limCC B ) <-> G e. ( ( J CnP K ) ` B ) ) )