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

Metamath Proof Explorer

Theorem limcmpt2

Description: Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcmpt2.a 
|- ( ph -> A C_ CC )
limcmpt2.b 
|- ( ph -> B e. A )
limcmpt2.f 
|- ( ( ph /\ ( z e. A /\ z =/= B ) ) -> D e. CC )
limcmpt2.j 
|- J = ( K |`t A )
limcmpt2.k 
|- K = ( TopOpen ` CCfld )
Assertion limcmpt2 
|- ( ph -> ( C e. ( ( z e. ( A \ { B } ) |-> D ) limCC B ) <-> ( z e. A |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 limcmpt2.a 
 |-  ( ph -> A C_ CC )
2 limcmpt2.b 
 |-  ( ph -> B e. A )
3 limcmpt2.f 
 |-  ( ( ph /\ ( z e. A /\ z =/= B ) ) -> D e. CC )
4 limcmpt2.j 
 |-  J = ( K |`t A )
5 limcmpt2.k 
 |-  K = ( TopOpen ` CCfld )
6 1 ssdifssd 
 |-  ( ph -> ( A \ { B } ) C_ CC )
7 1 2 sseldd 
 |-  ( ph -> B e. CC )
8 eldifsn 
 |-  ( z e. ( A \ { B } ) <-> ( z e. A /\ z =/= B ) )
9 8 3 sylan2b 
 |-  ( ( ph /\ z e. ( A \ { B } ) ) -> D e. CC )
10 eqid 
 |-  ( K |`t ( ( A \ { B } ) u. { B } ) ) = ( K |`t ( ( A \ { B } ) u. { B } ) )
11 6 7 9 10 5 limcmpt 
 |-  ( ph -> ( C e. ( ( z e. ( A \ { B } ) |-> D ) limCC B ) <-> ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( ( K |`t ( ( A \ { B } ) u. { B } ) ) CnP K ) ` B ) ) )
12 undif1 
 |-  ( ( A \ { B } ) u. { B } ) = ( A u. { B } )
13 2 snssd 
 |-  ( ph -> { B } C_ A )
14 ssequn2 
 |-  ( { B } C_ A <-> ( A u. { B } ) = A )
15 13 14 sylib 
 |-  ( ph -> ( A u. { B } ) = A )
16 12 15 eqtrid 
 |-  ( ph -> ( ( A \ { B } ) u. { B } ) = A )
17 16 mpteq1d 
 |-  ( ph -> ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , C , D ) ) = ( z e. A |-> if ( z = B , C , D ) ) )
18 16 oveq2d 
 |-  ( ph -> ( K |`t ( ( A \ { B } ) u. { B } ) ) = ( K |`t A ) )
19 18 4 eqtr4di 
 |-  ( ph -> ( K |`t ( ( A \ { B } ) u. { B } ) ) = J )
20 19 oveq1d 
 |-  ( ph -> ( ( K |`t ( ( A \ { B } ) u. { B } ) ) CnP K ) = ( J CnP K ) )
21 20 fveq1d 
 |-  ( ph -> ( ( ( K |`t ( ( A \ { B } ) u. { B } ) ) CnP K ) ` B ) = ( ( J CnP K ) ` B ) )
22 17 21 eleq12d 
 |-  ( ph -> ( ( z e. ( ( A \ { B } ) u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( ( K |`t ( ( A \ { B } ) u. { B } ) ) CnP K ) ` B ) <-> ( z e. A |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
23 11 22 bitrd 
 |-  ( ph -> ( C e. ( ( z e. ( A \ { B } ) |-> D ) limCC B ) <-> ( z e. A |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )