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 φ F : A D
limccnp.d φ D
limccnp.k K = TopOpen fld
limccnp.j J = K 𝑡 D
limccnp.c φ C F lim B
limccnp.b φ G J CnP K C
Assertion limccnp φ G C G F lim B

Proof

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