Metamath Proof Explorer

Theorem limccog

Description: Limit of the composition of two functions. If the limit of F at A is B and the limit of G at B is C , then the limit of G o. F at A is C . With respect to limcco and limccnp , here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limccog.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ ( dom 𝐺 ∖ { 𝐵 } ) )
limccog.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 limℂ 𝐴 ) )
limccog.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) )
Assertion limccog ( 𝜑 → 𝐶 ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 limccog.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ ( dom 𝐺 ∖ { 𝐵 } ) )
2 limccog.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 limℂ 𝐴 ) )
3 limccog.3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) )
4 limccl ⊢ ( 𝐺 limℂ 𝐵 ) ⊆ ℂ
5 4 3 sseldi ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 limcrcl ⊢ ( 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
7 3 6 syl ⊢ ( 𝜑 → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) )
8 7 simp1d ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℂ )
9 7 simp2d ⊢ ( 𝜑 → dom 𝐺 ⊆ ℂ )
10 7 simp3d ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 8 9 10 11 ellimc2 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
13 3 12 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
14 13 simprd ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
15 14 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
16 15 imp ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
17 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → 𝜑 )
18 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → 𝑣 ∈ ( TopOpen ‘ ℂfld ) )
19 simp3l ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → 𝐵 ∈ 𝑣 )
20 limcrcl ⊢ ( 𝐵 ∈ ( 𝐹 limℂ 𝐴 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐴 ∈ ℂ ) )
21 2 20 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐴 ∈ ℂ ) )
22 21 simp1d ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
23 21 simp2d ⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ )
24 21 simp3d ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
25 22 23 24 11 ellimc2 ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐹 limℂ 𝐴 ) ↔ ( 𝐵 ∈ ℂ ∧ ∀ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) ) ) ) )
26 2 25 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℂ ∧ ∀ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) ) ) )
27 26 simprd ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) ) )
28 27 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐵 ∈ 𝑣 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) ) )
29 28 imp ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑣 ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) )
30 17 18 19 29 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) )
31 imaco ⊢ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) = ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) )
32 17 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → 𝜑 )
33 simpl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 )
34 33 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 )
35 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 )
36 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 )
37 imassrn ⊢ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ ran 𝐹
38 37 1 sstrid ⊢ ( 𝜑 → ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ ( dom 𝐺 ∖ { 𝐵 } ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ ( dom 𝐺 ∖ { 𝐵 } ) )
40 36 39 ssind ⊢ ( ( 𝜑 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) )
41 imass2 ⊢ ( ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) → ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ) ⊆ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) )
42 40 41 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ) ⊆ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ) ⊆ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) )
44 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 )
45 43 44 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ) ⊆ 𝑢 )
46 32 34 35 45 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐺 “ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ) ⊆ 𝑢 )
47 31 46 eqsstrid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 )
48 47 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) → ( ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 → ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) )
49 48 anim2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ) → ( ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
50 49 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ( ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑣 ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
51 30 50 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) ∧ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) )
52 51 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) → ( ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐵 ∈ 𝑣 ∧ ( 𝐺 “ ( 𝑣 ∩ ( dom 𝐺 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
53 16 52 mpd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) ∧ 𝐶 ∈ 𝑢 ) → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) )
54 53 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) )
56 22 ffund ⊢ ( 𝜑 → Fun 𝐹 )
57 fdmrn ⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
58 56 57 sylib ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
59 1 difss2d ⊢ ( 𝜑 → ran 𝐹 ⊆ dom 𝐺 )
60 58 59 fssd ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ dom 𝐺 )
61 fco ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝐹 : dom 𝐹 ⟶ dom 𝐺 ) → ( 𝐺 ∘ 𝐹 ) : dom 𝐹 ⟶ ℂ )
62 8 60 61 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : dom 𝐹 ⟶ ℂ )
63 62 23 24 11 ellimc2 ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐴 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ( TopOpen ‘ ℂfld ) ( 𝐴 ∈ 𝑤 ∧ ( ( 𝐺 ∘ 𝐹 ) “ ( 𝑤 ∩ ( dom 𝐹 ∖ { 𝐴 } ) ) ) ⊆ 𝑢 ) ) ) ) )
64 5 55 63 mpbir2and ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐺 ∘ 𝐹 ) limℂ 𝐴 ) )