Metamath Proof Explorer

Theorem limccnp

Description: If the limit of F at B is C and G is continuous at C , then the limit of G o. F at B is G ( C ) . (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses limccnp.f 
|- ( ph -> F : A --> D )
limccnp.d 
|- ( ph -> D C_ CC )
limccnp.k 
|- K = ( TopOpen ` CCfld )
limccnp.j 
|- J = ( K |`t D )
limccnp.c 
|- ( ph -> C e. ( F limCC B ) )
limccnp.b 
|- ( ph -> G e. ( ( J CnP K ) ` C ) )
Assertion limccnp 
|- ( ph -> ( G ` C ) e. ( ( G o. F ) limCC B ) )

Proof

Step Hyp Ref Expression
1 limccnp.f 
 |-  ( ph -> F : A --> D )
2 limccnp.d 
 |-  ( ph -> D C_ CC )
3 limccnp.k 
 |-  K = ( TopOpen ` CCfld )
4 limccnp.j 
 |-  J = ( K |`t D )
5 limccnp.c 
 |-  ( ph -> C e. ( F limCC B ) )
6 limccnp.b 
 |-  ( ph -> G e. ( ( J CnP K ) ` C ) )
7 3 cnfldtopon 
 |-  K e. ( TopOn ` CC )
8 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ D C_ CC ) -> ( K |`t D ) e. ( TopOn ` D ) )
9 7 2 8 sylancr 
 |-  ( ph -> ( K |`t D ) e. ( TopOn ` D ) )
10 4 9 eqeltrid 
 |-  ( ph -> J e. ( TopOn ` D ) )
11 7 a1i 
 |-  ( ph -> K e. ( TopOn ` CC ) )
12 cnpf2 
 |-  ( ( J e. ( TopOn ` D ) /\ K e. ( TopOn ` CC ) /\ G e. ( ( J CnP K ) ` C ) ) -> G : D --> CC )
13 10 11 6 12 syl3anc 
 |-  ( ph -> G : D --> CC )
14 eqid 
 |-  U. J = U. J
15 14 cnprcl 
 |-  ( G e. ( ( J CnP K ) ` C ) -> C e. U. J )
16 6 15 syl 
 |-  ( ph -> C e. U. J )
17 toponuni 
 |-  ( J e. ( TopOn ` D ) -> D = U. J )
18 10 17 syl 
 |-  ( ph -> D = U. J )
19 16 18 eleqtrrd 
 |-  ( ph -> C e. D )
20 19 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ x = B ) -> C e. D )
21 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> F : A --> D )
22 elun 
 |-  ( x e. ( A u. { B } ) <-> ( x e. A \/ x e. { B } ) )
23 elsni 
 |-  ( x e. { B } -> x = B )
24 23 orim2i 
 |-  ( ( x e. A \/ x e. { B } ) -> ( x e. A \/ x = B ) )
25 22 24 sylbi 
 |-  ( x e. ( A u. { B } ) -> ( x e. A \/ x = B ) )
26 25 adantl 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( x e. A \/ x = B ) )
27 26 orcomd 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> ( x = B \/ x e. A ) )
28 27 orcanai 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> x e. A )
29 21 28 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> ( F ` x ) e. D )
30 20 29 ifclda 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , C , ( F ` x ) ) e. D )
31 13 30 cofmpt 
 |-  ( ph -> ( G o. ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ) = ( x e. ( A u. { B } ) |-> ( G ` if ( x = B , C , ( F ` x ) ) ) ) )
32 fvco3 
 |-  ( ( F : A --> D /\ x e. A ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
33 21 28 32 syl2anc 
 |-  ( ( ( ph /\ x e. ( A u. { B } ) ) /\ -. x = B ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
34 33 ifeq2da 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) = if ( x = B , ( G ` C ) , ( G ` ( F ` x ) ) ) )
35 fvif 
 |-  ( G ` if ( x = B , C , ( F ` x ) ) ) = if ( x = B , ( G ` C ) , ( G ` ( F ` x ) ) )
36 34 35 eqtr4di 
 |-  ( ( ph /\ x e. ( A u. { B } ) ) -> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) = ( G ` if ( x = B , C , ( F ` x ) ) ) )
37 36 mpteq2dva 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) ) = ( x e. ( A u. { B } ) |-> ( G ` if ( x = B , C , ( F ` x ) ) ) ) )
38 31 37 eqtr4d 
 |-  ( ph -> ( G o. ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ) = ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) ) )
39 eqid 
 |-  ( K |`t ( A u. { B } ) ) = ( K |`t ( A u. { B } ) )
40 eqid 
 |-  ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) = ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) )
41 1 2 fssd 
 |-  ( ph -> F : A --> CC )
42 1 fdmd 
 |-  ( ph -> dom F = A )
43 limcrcl 
 |-  ( C e. ( F limCC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
44 5 43 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
45 44 simp2d 
 |-  ( ph -> dom F C_ CC )
46 42 45 eqsstrrd 
 |-  ( ph -> A C_ CC )
47 44 simp3d 
 |-  ( ph -> B e. CC )
48 39 3 40 41 46 47 ellimc 
 |-  ( ph -> ( C e. ( F limCC B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
49 5 48 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
50 3 cnfldtop 
 |-  K e. Top
51 50 a1i 
 |-  ( ph -> K e. Top )
52 30 fmpttd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) : ( A u. { B } ) --> D )
53 47 snssd 
 |-  ( ph -> { B } C_ CC )
54 46 53 unssd 
 |-  ( ph -> ( A u. { B } ) C_ CC )
55 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ ( A u. { B } ) C_ CC ) -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
56 7 54 55 sylancr 
 |-  ( ph -> ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) )
57 toponuni 
 |-  ( ( K |`t ( A u. { B } ) ) e. ( TopOn ` ( A u. { B } ) ) -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
58 56 57 syl 
 |-  ( ph -> ( A u. { B } ) = U. ( K |`t ( A u. { B } ) ) )
59 58 feq2d 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) : ( A u. { B } ) --> D <-> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) : U. ( K |`t ( A u. { B } ) ) --> D ) )
60 52 59 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) : U. ( K |`t ( A u. { B } ) ) --> D )
61 eqid 
 |-  U. ( K |`t ( A u. { B } ) ) = U. ( K |`t ( A u. { B } ) )
62 7 toponunii 
 |-  CC = U. K
63 61 62 cnprest2 
 |-  ( ( K e. Top /\ ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) : U. ( K |`t ( A u. { B } ) ) --> D /\ D C_ CC ) -> ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K |`t D ) ) ` B ) ) )
64 51 60 2 63 syl3anc 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K |`t D ) ) ` B ) ) )
65 49 64 mpbid 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP ( K |`t D ) ) ` B ) )
66 4 oveq2i 
 |-  ( ( K |`t ( A u. { B } ) ) CnP J ) = ( ( K |`t ( A u. { B } ) ) CnP ( K |`t D ) )
67 66 fveq1i 
 |-  ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) = ( ( ( K |`t ( A u. { B } ) ) CnP ( K |`t D ) ) ` B )
68 65 67 eleqtrrdi 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) )
69 iftrue 
 |-  ( x = B -> if ( x = B , C , ( F ` x ) ) = C )
70 ssun2 
 |-  { B } C_ ( A u. { B } )
71 snssg 
 |-  ( B e. CC -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
72 47 71 syl 
 |-  ( ph -> ( B e. ( A u. { B } ) <-> { B } C_ ( A u. { B } ) ) )
73 70 72 mpbiri 
 |-  ( ph -> B e. ( A u. { B } ) )
74 40 69 73 5 fvmptd3 
 |-  ( ph -> ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ` B ) = C )
75 74 fveq2d 
 |-  ( ph -> ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ` B ) ) = ( ( J CnP K ) ` C ) )
76 6 75 eleqtrrd 
 |-  ( ph -> G e. ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ` B ) ) )
77 cnpco 
 |-  ( ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP J ) ` B ) /\ G e. ( ( J CnP K ) ` ( ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ` B ) ) ) -> ( G o. ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
78 68 76 77 syl2anc 
 |-  ( ph -> ( G o. ( x e. ( A u. { B } ) |-> if ( x = B , C , ( F ` x ) ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
79 38 78 eqeltrrd 
 |-  ( ph -> ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
80 eqid 
 |-  ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) ) = ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) )
81 fco 
 |-  ( ( G : D --> CC /\ F : A --> D ) -> ( G o. F ) : A --> CC )
82 13 1 81 syl2anc 
 |-  ( ph -> ( G o. F ) : A --> CC )
83 39 3 80 82 46 47 ellimc 
 |-  ( ph -> ( ( G ` C ) e. ( ( G o. F ) limCC B ) <-> ( x e. ( A u. { B } ) |-> if ( x = B , ( G ` C ) , ( ( G o. F ) ` x ) ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
84 79 83 mpbird 
 |-  ( ph -> ( G ` C ) e. ( ( G o. F ) limCC B ) )