Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → 𝑟 ∈ ℝ+) |
2 | | equivcau.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
3 | 2 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → 𝑅 ∈
ℝ+) |
4 | 1, 3 | rpdivcld 11889 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → (𝑟 / 𝑅) ∈
ℝ+) |
5 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑠 = (𝑟 / 𝑅) → ((𝑓‘𝑘)(ball‘𝐷)𝑠) = ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
6 | 5 | feq3d 6032 |
. . . . . . . 8
⊢ (𝑠 = (𝑟 / 𝑅) → ((𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) ↔ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
7 | 6 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑠 = (𝑟 / 𝑅) → (∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) ↔ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
8 | 7 | rspcv 3305 |
. . . . . 6
⊢ ((𝑟 / 𝑅) ∈ ℝ+ →
(∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
9 | 4, 8 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → (∀𝑠 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
10 | | simprr 796 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
11 | | elpmi 7876 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑋 ↑pm ℂ) →
(𝑓:dom 𝑓⟶𝑋 ∧ dom 𝑓 ⊆ ℂ)) |
12 | 11 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑋 ↑pm ℂ) →
𝑓:dom 𝑓⟶𝑋) |
13 | 12 | ad3antlr 767 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑓:dom 𝑓⟶𝑋) |
14 | | resss 5422 |
. . . . . . . . . . . 12
⊢ (𝑓 ↾
(ℤ≥‘𝑘)) ⊆ 𝑓 |
15 | | dmss 5323 |
. . . . . . . . . . . 12
⊢ ((𝑓 ↾
(ℤ≥‘𝑘)) ⊆ 𝑓 → dom (𝑓 ↾ (ℤ≥‘𝑘)) ⊆ dom 𝑓) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom
(𝑓 ↾
(ℤ≥‘𝑘)) ⊆ dom 𝑓 |
17 | | uzid 11702 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
(ℤ≥‘𝑘)) |
18 | 17 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ (ℤ≥‘𝑘)) |
19 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → dom (𝑓 ↾ (ℤ≥‘𝑘)) =
(ℤ≥‘𝑘)) |
20 | 19 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → dom (𝑓 ↾ (ℤ≥‘𝑘)) =
(ℤ≥‘𝑘)) |
21 | 18, 20 | eleqtrrd 2704 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ dom (𝑓 ↾ (ℤ≥‘𝑘))) |
22 | 16, 21 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ dom 𝑓) |
23 | 13, 22 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓‘𝑘) ∈ 𝑋) |
24 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘𝐶) =
(MetOpen‘𝐶) |
25 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
26 | | equivcau.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) |
27 | | equivcau.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
28 | | equivcau.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) |
29 | 24, 25, 26, 27, 2, 28 | metss2lem 22316 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) |
30 | 29 | expr 643 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
31 | 30 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
32 | 31 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → ∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
33 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑟 ∈ ℝ+) |
34 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓‘𝑘) → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) = ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
35 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓‘𝑘) → (𝑥(ball‘𝐶)𝑟) = ((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
36 | 34, 35 | sseq12d 3634 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟) ↔ ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
37 | 36 | imbi2d 330 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) ↔ (𝑟 ∈ ℝ+ → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)))) |
38 | 37 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝑓‘𝑘) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) → (𝑟 ∈ ℝ+ → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)))) |
39 | 23, 32, 33, 38 | syl3c 66 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
40 | 10, 39 | fssd 6057 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ (𝑘 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
41 | 40 | expr 643 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) ∧ 𝑘 ∈ ℤ) → ((𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
42 | 41 | reximdva 3017 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → (∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
43 | 9, 42 | syld 47 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧
𝑟 ∈
ℝ+) → (∀𝑠 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
44 | 43 | ralrimdva 2969 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
45 | 44 | ss2rabdv 3683 |
. 2
⊢ (𝜑 → {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)} ⊆ {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
46 | | metxmet 22139 |
. . 3
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
47 | | caufval 23073 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)}) |
48 | 27, 46, 47 | 3syl 18 |
. 2
⊢ (𝜑 → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)}) |
49 | | metxmet 22139 |
. . 3
⊢ (𝐶 ∈ (Met‘𝑋) → 𝐶 ∈ (∞Met‘𝑋)) |
50 | | caufval 23073 |
. . 3
⊢ (𝐶 ∈ (∞Met‘𝑋) → (Cau‘𝐶) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
51 | 26, 49, 50 | 3syl 18 |
. 2
⊢ (𝜑 → (Cau‘𝐶) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
52 | 45, 48, 51 | 3sstr4d 3648 |
1
⊢ (𝜑 → (Cau‘𝐷) ⊆ (Cau‘𝐶)) |