Step | Hyp | Ref
| Expression |
1 | | cncfco.5 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶)) |
2 | | cncff 24054 |
. . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐺:𝐵⟶𝐶) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:𝐵⟶𝐶) |
4 | | cncfco.4 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) |
5 | | cncff 24054 |
. . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
7 | | fco 6622 |
. . 3
⊢ ((𝐺:𝐵⟶𝐶 ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶𝐶) |
8 | 3, 6, 7 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹):𝐴⟶𝐶) |
9 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐺 ∈ (𝐵–cn→𝐶)) |
10 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐹:𝐴⟶𝐵) |
11 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ 𝐴) |
12 | 10, 11 | ffvelrnd 6959 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → (𝐹‘𝑥) ∈ 𝐵) |
13 | | simprr 770 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈
ℝ+) |
14 | | cncfi 24055 |
. . . . 5
⊢ ((𝐺 ∈ (𝐵–cn→𝐶) ∧ (𝐹‘𝑥) ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
15 | 9, 12, 13, 14 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
16 | 4 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝐹 ∈ (𝐴–cn→𝐵)) |
17 | | simplrl 774 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑥 ∈ 𝐴) |
18 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑢 ∈
ℝ+) |
19 | | cncfi 24055 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
20 | 16, 17, 18, 19 | syl3anc 1370 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
21 | 6 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝐹:𝐴⟶𝐵) |
22 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑤 ∈ 𝐴) |
23 | 21, 22 | ffvelrnd 6959 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (𝐹‘𝑤) ∈ 𝐵) |
24 | | fvoveq1 7294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐹‘𝑤) → (abs‘(𝑣 − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥)))) |
25 | 24 | breq1d 5089 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
26 | 25 | imbrov2fvoveq 7296 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝐹‘𝑤) → (((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
27 | 26 | rspcv 3556 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) ∈ 𝐵 → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
29 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) |
30 | 21, 22, 29 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) |
31 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑥 ∈ 𝐴) |
32 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
33 | 21, 31, 32 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
34 | 30, 33 | oveq12d 7289 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥)) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) |
35 | 34 | fveq2d 6775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))) |
36 | 35 | breq1d 5089 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
((abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
37 | 36 | imbi2d 341 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
38 | 28, 37 | sylibrd 258 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
39 | 38 | imp 407 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) ∧
∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
40 | 39 | an32s 649 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
41 | 40 | imim2d 57 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
42 | 41 | anassrs 468 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ 𝐴) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
43 | 42 | ralimdva 3105 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) →
(∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
44 | 43 | reximdva 3205 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
45 | 44 | ex 413 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
46 | 20, 45 | mpid 44 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
47 | 46 | rexlimdva 3215 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
(∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
48 | 15, 47 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
49 | 48 | ralrimivva 3117 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
50 | | cncfrss 24052 |
. . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
51 | 4, 50 | syl 17 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
52 | | cncfrss2 24053 |
. . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐶 ⊆ ℂ) |
53 | 1, 52 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ⊆ ℂ) |
54 | | elcncf2 24051 |
. . 3
⊢ ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
55 | 51, 53, 54 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
56 | 8, 49, 55 | mpbir2and 710 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶)) |