Step | Hyp | Ref
| Expression |
1 | | cncfco.5 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶)) |
2 | | cncff 22504 |
. . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐺:𝐵⟶𝐶) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:𝐵⟶𝐶) |
4 | | cncfco.4 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) |
5 | | cncff 22504 |
. . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
7 | | fco 5971 |
. . 3
⊢ ((𝐺:𝐵⟶𝐶 ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶𝐶) |
8 | 3, 6, 7 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹):𝐴⟶𝐶) |
9 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐺 ∈ (𝐵–cn→𝐶)) |
10 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝐹:𝐴⟶𝐵) |
11 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ 𝐴) |
12 | 10, 11 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → (𝐹‘𝑥) ∈ 𝐵) |
13 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈
ℝ+) |
14 | | cncfi 22505 |
. . . . 5
⊢ ((𝐺 ∈ (𝐵–cn→𝐶) ∧ (𝐹‘𝑥) ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
15 | 9, 12, 13, 14 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
16 | 4 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝐹 ∈ (𝐴–cn→𝐵)) |
17 | | simplrl 796 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑥 ∈ 𝐴) |
18 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ 𝑢 ∈
ℝ+) |
19 | | cncfi 22505 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
20 | 16, 17, 18, 19 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
21 | 6 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝐹:𝐴⟶𝐵) |
22 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑤 ∈ 𝐴) |
23 | 21, 22 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (𝐹‘𝑤) ∈ 𝐵) |
24 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐹‘𝑤) → (𝑣 − (𝐹‘𝑥)) = ((𝐹‘𝑤) − (𝐹‘𝑥))) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐹‘𝑤) → (abs‘(𝑣 − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑤) − (𝐹‘𝑥)))) |
26 | 25 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 ↔ (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢)) |
27 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐹‘𝑤) → (𝐺‘𝑣) = (𝐺‘(𝐹‘𝑤))) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐹‘𝑤) → ((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥))) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐹‘𝑤) → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))) |
30 | 29 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝐹‘𝑤) → ((abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
31 | 26, 30 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝐹‘𝑤) → (((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
32 | 31 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) ∈ 𝐵 → (∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
33 | 23, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
34 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) |
35 | 21, 22, 34 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑤) = (𝐺‘(𝐹‘𝑤))) |
36 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → 𝑥 ∈ 𝐴) |
37 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
38 | 21, 36, 37 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
39 | 35, 38 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) → (((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥)) = ((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) = (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥))))) |
41 | 40 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
((abs‘(((𝐺 ∘
𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦 ↔ (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) |
42 | 41 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦) ↔ ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘(𝐹‘𝑤)) − (𝐺‘(𝐹‘𝑥)))) < 𝑦))) |
43 | 33, 42 | sylibrd 248 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) →
(∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
44 | 43 | imp 444 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ (𝑧 ∈
ℝ+ ∧ 𝑤
∈ 𝐴)) ∧
∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
45 | 44 | an32s 842 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → ((abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
46 | 45 | imim2d 55 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ (𝑧 ∈ ℝ+ ∧ 𝑤 ∈ 𝐴)) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
47 | 46 | anassrs 678 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ 𝐴) → (((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
48 | 47 | ralimdva 2945 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) ∧ 𝑧 ∈ ℝ+) →
(∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
49 | 48 | reximdva 3000 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
∧ ∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦)) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
50 | 49 | ex 449 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → (∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑢) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
51 | 20, 50 | mpid 43 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) ∧ 𝑢 ∈ ℝ+)
→ (∀𝑣 ∈
𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
52 | 51 | rexlimdva 3013 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
(∃𝑢 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑣 − (𝐹‘𝑥))) < 𝑢 → (abs‘((𝐺‘𝑣) − (𝐺‘(𝐹‘𝑥)))) < 𝑦) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦))) |
53 | 15, 52 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
54 | 53 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)) |
55 | | cncfrss 22502 |
. . . 4
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
56 | 4, 55 | syl 17 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
57 | | cncfrss2 22503 |
. . . 4
⊢ (𝐺 ∈ (𝐵–cn→𝐶) → 𝐶 ⊆ ℂ) |
58 | 1, 57 | syl 17 |
. . 3
⊢ (𝜑 → 𝐶 ⊆ ℂ) |
59 | | elcncf2 22501 |
. . 3
⊢ ((𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ) → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
60 | 56, 58, 59 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶) ↔ ((𝐺 ∘ 𝐹):𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘(((𝐺 ∘ 𝐹)‘𝑤) − ((𝐺 ∘ 𝐹)‘𝑥))) < 𝑦)))) |
61 | 8, 54, 60 | mpbir2and 959 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶)) |