# 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 ${⊢}{\phi }\to {F}:{A}⟶{D}$
limccnp.d ${⊢}{\phi }\to {D}\subseteq ℂ$
limccnp.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
limccnp.j ${⊢}{J}={K}{↾}_{𝑡}{D}$
limccnp.c ${⊢}{\phi }\to {C}\in \left({F}{lim}_{ℂ}{B}\right)$
limccnp.b ${⊢}{\phi }\to {G}\in \left({J}\mathrm{CnP}{K}\right)\left({C}\right)$
Assertion limccnp ${⊢}{\phi }\to {G}\left({C}\right)\in \left(\left({G}\circ {F}\right){lim}_{ℂ}{B}\right)$

### Proof

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