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	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
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	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
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→ 𝐶 ) )