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∈FlimℂB
limccnp.b ⊢φ→G∈JCnPK⁡C
Assertion limccnp ⊢φ→G⁡C∈G∘Flimℂ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∈FlimℂB
6 limccnp.b ⊢φ→G∈JCnPK⁡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∈JCnPK⁡C→G:D⟶ℂ
13 10 11 6 12 syl3anc ⊢φ→G:D⟶ℂ
14 eqid ⊢⋃J=⋃J
15 14 cnprcl ⊢G∈JCnPK⁡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 ffvelcdmd ⊢φ∧x∈A∪B∧¬x=B→F⁡x∈D
30 20 29 ifclda ⊢φ∧x∈A∪B→ifx=BCF⁡x∈D
31 13 30 cofmpt ⊢φ→G∘x∈A∪B⟼ifx=BCF⁡x=x∈A∪B⟼G⁡ifx=BCF⁡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→ifx=BG⁡CG∘F⁡x=ifx=BG⁡CG⁡F⁡x
35 fvif ⊢G⁡ifx=BCF⁡x=ifx=BG⁡CG⁡F⁡x
36 34 35 eqtr4di ⊢φ∧x∈A∪B→ifx=BG⁡CG∘F⁡x=G⁡ifx=BCF⁡x
37 36 mpteq2dva ⊢φ→x∈A∪B⟼ifx=BG⁡CG∘F⁡x=x∈A∪B⟼G⁡ifx=BCF⁡x
38 31 37 eqtr4d ⊢φ→G∘x∈A∪B⟼ifx=BCF⁡x=x∈A∪B⟼ifx=BG⁡CG∘F⁡x
39 eqid ⊢K↾𝑡A∪B=K↾𝑡A∪B
40 eqid ⊢x∈A∪B⟼ifx=BCF⁡x=x∈A∪B⟼ifx=BCF⁡x
41 1 2 fssd ⊢φ→F:A⟶ℂ
42 1 fdmd ⊢φ→dom⁡F=A
43 limcrcl ⊢C∈Flimℂ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∈FlimℂB↔x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B
49 5 48 mpbid ⊢φ→x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B
50 3 cnfldtop ⊢K∈Top
51 50 a1i ⊢φ→K∈Top
52 30 fmpttd ⊢φ→x∈A∪B⟼ifx=BCF⁡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⟼ifx=BCF⁡x:A∪B⟶D↔x∈A∪B⟼ifx=BCF⁡x:⋃K↾𝑡A∪B⟶D
60 52 59 mpbid ⊢φ→x∈A∪B⟼ifx=BCF⁡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⟼ifx=BCF⁡x:⋃K↾𝑡A∪B⟶D∧D⊆ℂ→x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B↔x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK↾𝑡D⁡B
64 51 60 2 63 syl3anc ⊢φ→x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B↔x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK↾𝑡D⁡B
65 49 64 mpbid ⊢φ→x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK↾𝑡D⁡B
66 4 oveq2i ⊢K↾𝑡A∪BCnPJ=K↾𝑡A∪BCnPK↾𝑡D
67 66 fveq1i ⊢K↾𝑡A∪BCnPJ⁡B=K↾𝑡A∪BCnPK↾𝑡D⁡B
68 65 67 eleqtrrdi ⊢φ→x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPJ⁡B
69 iftrue ⊢x=B→ifx=BCF⁡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⟼ifx=BCF⁡x⁡B=C
75 74 fveq2d ⊢φ→JCnPK⁡x∈A∪B⟼ifx=BCF⁡x⁡B=JCnPK⁡C
76 6 75 eleqtrrd ⊢φ→G∈JCnPK⁡x∈A∪B⟼ifx=BCF⁡x⁡B
77 cnpco ⊢x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPJ⁡B∧G∈JCnPK⁡x∈A∪B⟼ifx=BCF⁡x⁡B→G∘x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B
78 68 76 77 syl2anc ⊢φ→G∘x∈A∪B⟼ifx=BCF⁡x∈K↾𝑡A∪BCnPK⁡B
79 38 78 eqeltrrd ⊢φ→x∈A∪B⟼ifx=BG⁡CG∘F⁡x∈K↾𝑡A∪BCnPK⁡B
80 eqid ⊢x∈A∪B⟼ifx=BG⁡CG∘F⁡x=x∈A∪B⟼ifx=BG⁡CG∘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∘FlimℂB↔x∈A∪B⟼ifx=BG⁡CG∘F⁡x∈K↾𝑡A∪BCnPK⁡B
84 79 83 mpbird ⊢φ→G⁡C∈G∘FlimℂB