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 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𝐶 ) )