| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cncfco.5 | . . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶)) | 
| 2 |  | cncff 24920 | . . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐺:𝐵⟶𝐶) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝜑 → 𝐺:𝐵⟶𝐶) | 
| 4 |  | cncfco.4 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) | 
| 5 |  | cncff 24920 | . . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 7 |  | fco 6759 | . . 3
⊢ ((𝐺:𝐵⟶𝐶 ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶𝐶) | 
| 8 | 3, 6, 7 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐺 ∘ 𝐹):𝐴⟶𝐶) | 
| 9 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐺 ∈ (𝐵–cn→𝐶)) | 
| 10 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐹:𝐴⟶𝐵) | 
| 11 |  | simprl 770 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ 𝐴) | 
| 12 | 10, 11 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → (𝐹‘𝑥) ∈ 𝐵) | 
| 13 |  | simprr 772 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈
ℝ+) | 
| 14 |  | cncfi 24921 | . . . . 5
⊢ ((𝐺 ∈ (𝐵–cn→𝐶) ∧ (𝐹‘𝑥) ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) | 
| 15 | 9, 12, 13, 14 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) | 
| 16 | 4 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝐹 ∈ (𝐴–cn→𝐵)) | 
| 17 |  | simplrl 776 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑥 ∈ 𝐴) | 
| 18 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑢 ∈
ℝ+) | 
| 19 |  | cncfi 24921 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) | 
| 20 | 16, 17, 18, 19 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) | 
| 21 | 6 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝐹:𝐴⟶𝐵) | 
| 22 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑤 ∈ 𝐴) | 
| 23 | 21, 22 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (𝐹‘𝑤) ∈ 𝐵) | 
| 24 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐹‘𝑤) → (abs‘(𝑣 − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥)))) | 
| 25 | 24 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) | 
| 26 | 25 | imbrov2fvoveq 7457 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝐹‘𝑤) → (((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) | 
| 27 | 26 | rspcv 3617 | . . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) ∈ 𝐵 → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) | 
| 28 | 23, 27 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) | 
| 29 |  | fvco3 7007 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) | 
| 30 | 21, 22, 29 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) | 
| 31 | 17 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑥 ∈ 𝐴) | 
| 32 |  | fvco3 7007 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) | 
| 33 | 21, 31, 32 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) | 
| 34 | 30, 33 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥)) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) | 
| 35 | 34 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))) | 
| 36 | 35 | breq1d 5152 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
((abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) | 
| 37 | 36 | imbi2d 340 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) | 
| 38 | 28, 37 | sylibrd 259 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 39 | 38 | imp 406 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) ∧
∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) | 
| 40 | 39 | an32s 652 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) | 
| 41 | 40 | imim2d 57 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 42 | 41 | anassrs 467 | . . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ 𝐴) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 43 | 42 | ralimdva 3166 | . . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) →
(∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 44 | 43 | reximdva 3167 | . . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 45 | 44 | ex 412 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) | 
| 46 | 20, 45 | mpid 44 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 47 | 46 | rexlimdva 3154 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
(∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) | 
| 48 | 15, 47 | mpd 15 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) | 
| 49 | 48 | ralrimivva 3201 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) | 
| 50 |  | cncfrss 24918 | . . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | 
| 51 | 4, 50 | syl 17 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 52 |  | cncfrss2 24919 | . . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐶 ⊆ ℂ) | 
| 53 | 1, 52 | syl 17 | . . 3
⊢ (𝜑 → 𝐶 ⊆ ℂ) | 
| 54 |  | elcncf2 24917 | . . 3
⊢ ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) | 
| 55 | 51, 53, 54 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) | 
| 56 | 8, 49, 55 | mpbir2and 713 | 1
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶)) |