This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐷 )
limccnp.d ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
limccnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limccnp.j ⊢ 𝐽 = ( 𝐾 ↾t 𝐷 )
limccnp.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) )
limccnp.b ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐶 ) )
Assertion limccnp ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limccnp.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐷 )
2 limccnp.d ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
3 limccnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4 limccnp.j ⊢ 𝐽 = ( 𝐾 ↾t 𝐷 )
5 limccnp.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) )
6 limccnp.b ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐶 ) )
7 3 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
8 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐾 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
9 7 2 8 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
10 4 9 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐷 ) )
11 7 a1i ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℂ ) )
12 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐷 ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐶 ) ) → 𝐺 : 𝐷 ⟶ ℂ )
13 10 11 6 12 syl3anc ⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℂ )
14 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
15 14 cnprcl ⊢ ( 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐶 ) → 𝐶 ∈ ∪ 𝐽 )
16 6 15 syl ⊢ ( 𝜑 → 𝐶 ∈ ∪ 𝐽 )
17 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐷 ) → 𝐷 = ∪ 𝐽 )
18 10 17 syl ⊢ ( 𝜑 → 𝐷 = ∪ 𝐽 )
19 16 18 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝑥 = 𝐵 ) → 𝐶 ∈ 𝐷 )
21 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐷 )
22 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐵 } ) )
23 elsni ⊢ ( 𝑥 ∈ { 𝐵 } → 𝑥 = 𝐵 )
24 23 orim2i ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐵 } ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵 ) )
25 22 24 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵 ) )
27 26 orcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝑥 = 𝐵 ∨ 𝑥 ∈ 𝐴 ) )
28 27 orcanai ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐴 )
29 21 28 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
30 20 29 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐷 )
31 13 30 cofmpt ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐺 ‘ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
32 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐷 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
33 21 28 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 33 ifeq2da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) = if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
35 fvif ⊢ ( 𝐺 ‘ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
36 34 35 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝐺 ‘ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) )
37 36 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ ( 𝐺 ‘ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
38 31 37 eqtr4d ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) )
39 eqid ⊢ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
40 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) )
41 1 2 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
42 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
43 limcrcl ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
44 5 43 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
45 44 simp2d ⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ )
46 42 45 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
47 44 simp3d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
48 39 3 40 41 46 47 ellimc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
49 5 48 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
50 3 cnfldtop ⊢ 𝐾 ∈ Top
51 50 a1i ⊢ ( 𝜑 → 𝐾 ∈ Top )
52 30 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ 𝐷 )
53 47 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ℂ )
54 46 53 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
55 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
56 7 54 55 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
57 toponuni ⊢ ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝐴 ∪ { 𝐵 } ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) )
58 56 57 syl ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) )
59 58 feq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ 𝐷 ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ 𝐷 ) )
60 52 59 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ 𝐷 )
61 eqid ⊢ ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
62 7 toponunii ⊢ ℂ = ∪ 𝐾
63 61 62 cnprest2 ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) : ∪ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ⟶ 𝐷 ∧ 𝐷 ⊆ ℂ ) → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ↾t 𝐷 ) ) ‘ 𝐵 ) ) )
64 51 60 2 63 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ↾t 𝐷 ) ) ‘ 𝐵 ) ) )
65 49 64 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ↾t 𝐷 ) ) ‘ 𝐵 ) )
66 4 oveq2i ⊢ ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) = ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ↾t 𝐷 ) )
67 66 fveq1i ⊢ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) = ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP ( 𝐾 ↾t 𝐷 ) ) ‘ 𝐵 )
68 65 67 eleqtrrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) )
69 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) = 𝐶 )
70 ssun2 ⊢ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } )
71 snssg ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
72 47 71 syl ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
73 70 72 mpbiri ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
74 40 69 73 5 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = 𝐶 )
75 74 fveq2d ⊢ ( 𝜑 → ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) ) = ( ( 𝐽 CnP 𝐾 ) ‘ 𝐶 ) )
76 6 75 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) ) )
77 cnpco ⊢ ( ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐽 ) ‘ 𝐵 ) ∧ 𝐺 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) ) ) → ( 𝐺 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
78 68 76 77 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
79 38 78 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) )
80 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) )
81 fco ⊢ ( ( 𝐺 : 𝐷 ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
82 13 1 81 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
83 39 3 80 82 46 47 ellimc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐶 ) ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐵 ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑥 = 𝐵 , ( 𝐺 ‘ 𝐶 ) , ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
84 79 83 mpbird ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐵 ) )