Metamath Proof Explorer

Theorem limcmpt

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

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

Proof

Step Hyp Ref Expression
1 limcmpt.a 
 |-  ( ph -> A C_ CC )
2 limcmpt.b 
 |-  ( ph -> B e. CC )
3 limcmpt.f 
 |-  ( ( ph /\ z e. A ) -> D e. CC )
4 limcmpt.j 
 |-  J = ( K |`t ( A u. { B } ) )
5 limcmpt.k 
 |-  K = ( TopOpen ` CCfld )
6 nfcv 
 |-  F/_ y if ( z = B , C , ( ( z e. A |-> D ) ` z ) )
7 nfv 
 |-  F/ z y = B
8 nfcv 
 |-  F/_ z C
9 nffvmpt1 
 |-  F/_ z ( ( z e. A |-> D ) ` y )
10 7 8 9 nfif 
 |-  F/_ z if ( y = B , C , ( ( z e. A |-> D ) ` y ) )
11 eqeq1 
 |-  ( z = y -> ( z = B <-> y = B ) )
12 fveq2 
 |-  ( z = y -> ( ( z e. A |-> D ) ` z ) = ( ( z e. A |-> D ) ` y ) )
13 11 12 ifbieq2d 
 |-  ( z = y -> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) = if ( y = B , C , ( ( z e. A |-> D ) ` y ) ) )
14 6 10 13 cbvmpt 
 |-  ( z e. ( A u. { B } ) |-> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) ) = ( y e. ( A u. { B } ) |-> if ( y = B , C , ( ( z e. A |-> D ) ` y ) ) )
15 3 fmpttd 
 |-  ( ph -> ( z e. A |-> D ) : A --> CC )
16 4 5 14 15 1 2 ellimc 
 |-  ( ph -> ( C e. ( ( z e. A |-> D ) limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) ) e. ( ( J CnP K ) ` B ) ) )
17 elun 
 |-  ( z e. ( A u. { B } ) <-> ( z e. A \/ z e. { B } ) )
18 velsn 
 |-  ( z e. { B } <-> z = B )
19 18 orbi2i 
 |-  ( ( z e. A \/ z e. { B } ) <-> ( z e. A \/ z = B ) )
20 17 19 bitri 
 |-  ( z e. ( A u. { B } ) <-> ( z e. A \/ z = B ) )
21 pm5.61 
 |-  ( ( ( z e. A \/ z = B ) /\ -. z = B ) <-> ( z e. A /\ -. z = B ) )
22 21 simplbi 
 |-  ( ( ( z e. A \/ z = B ) /\ -. z = B ) -> z e. A )
23 20 22 sylanb 
 |-  ( ( z e. ( A u. { B } ) /\ -. z = B ) -> z e. A )
24 23 3 sylan2 
 |-  ( ( ph /\ ( z e. ( A u. { B } ) /\ -. z = B ) ) -> D e. CC )
25 eqid 
 |-  ( z e. A |-> D ) = ( z e. A |-> D )
26 25 fvmpt2 
 |-  ( ( z e. A /\ D e. CC ) -> ( ( z e. A |-> D ) ` z ) = D )
27 23 24 26 syl2an2 
 |-  ( ( ph /\ ( z e. ( A u. { B } ) /\ -. z = B ) ) -> ( ( z e. A |-> D ) ` z ) = D )
28 27 anassrs 
 |-  ( ( ( ph /\ z e. ( A u. { B } ) ) /\ -. z = B ) -> ( ( z e. A |-> D ) ` z ) = D )
29 28 ifeq2da 
 |-  ( ( ph /\ z e. ( A u. { B } ) ) -> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) = if ( z = B , C , D ) )
30 29 mpteq2dva 
 |-  ( ph -> ( z e. ( A u. { B } ) |-> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) ) = ( z e. ( A u. { B } ) |-> if ( z = B , C , D ) ) )
31 30 eleq1d 
 |-  ( ph -> ( ( z e. ( A u. { B } ) |-> if ( z = B , C , ( ( z e. A |-> D ) ` z ) ) ) e. ( ( J CnP K ) ` B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
32 16 31 bitrd 
 |-  ( ph -> ( C e. ( ( z e. A |-> D ) limCC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )