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 eqtr4di ⊢ φ ∧ 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 eleqtrrdi ⊢ φ → 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