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

Metamath Proof Explorer

Theorem cncfco

Description: The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses cncfco.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
cncfco.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) )
Assertion cncfco ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐴 –cn→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cncfco.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
2 cncfco.5 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) )
3 cncff ⊢ ( 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) → 𝐺 : 𝐵 ⟶ 𝐶 )
4 2 3 syl ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
5 cncff ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
6 1 5 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 fco ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 )
8 4 6 7 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) )
10 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ 𝐴 )
12 10 11 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ+ )
14 cncfi ⊢ ( ( 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) )
15 9 12 13 14 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) )
16 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
17 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → 𝑥 ∈ 𝐴 )
18 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → 𝑢 ∈ ℝ+ )
19 cncfi ⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) )
21 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
22 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 )
23 21 22 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
24 fvoveq1 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑤 ) → ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
25 24 breq1d ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑤 ) → ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) )
26 25 imbrov2fvoveq ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑤 ) → ( ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) )
27 26 rspcv ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 → ( ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) )
28 23 27 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) )
29 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) )
30 21 22 29 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) )
31 17 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
32 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
33 21 31 32 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 30 33 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
35 34 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
36 35 breq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) )
37 36 imbi2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ ( 𝐹 ‘ 𝑤 ) ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) )
38 28 37 sylibrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
39 38 imp ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) )
40 39 an32s ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) )
41 40 imim2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
42 41 anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ 𝐴 ) → ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
43 42 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) → ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
44 43 reximdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
45 44 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
46 20 45 mpid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
47 46 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ( ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ 𝐵 ( ( abs ‘ ( 𝑣 − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑢 → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) < 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
48 15 47 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) )
49 48 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) )
50 cncfrss ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ )
51 1 50 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
52 cncfrss2 ⊢ ( 𝐺 ∈ ( 𝐵 –cn→ 𝐶 ) → 𝐶 ⊆ ℂ )
53 2 52 syl ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
54 elcncf2 ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ ) → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐴 –cn→ 𝐶 ) ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
55 51 53 54 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐴 –cn→ 𝐶 ) ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑤 ) − ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
56 8 49 55 mpbir2and ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ ( 𝐴 –cn→ 𝐶 ) )