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

Metamath Proof Explorer

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