Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ 𝑟 ∈
ℝ+) |
2 | | equivcau.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
3 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ 𝑅 ∈
ℝ+) |
4 | 1, 3 | rpdivcld 12645 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ (𝑟 / 𝑅) ∈
ℝ+) |
5 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑠 = (𝑟 / 𝑅) → ((𝑓‘𝑘)(ball‘𝐷)𝑠) = ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
6 | 5 | feq3d 6532 |
. . . . . . . 8
⊢ (𝑠 = (𝑟 / 𝑅) → ((𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) ↔ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
7 | 6 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑠 = (𝑟 / 𝑅) → (∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) ↔ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
8 | 7 | rspcv 3532 |
. . . . . 6
⊢ ((𝑟 / 𝑅) ∈ ℝ+ →
(∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
9 | 4, 8 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) |
10 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
11 | | elpmi 8527 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑋 ↑pm ℂ) → (𝑓:dom 𝑓⟶𝑋 ∧ dom 𝑓 ⊆ ℂ)) |
12 | 11 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑋 ↑pm ℂ) → 𝑓:dom 𝑓⟶𝑋) |
13 | 12 | ad3antlr 731 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑓:dom 𝑓⟶𝑋) |
14 | | resss 5876 |
. . . . . . . . . . . 12
⊢ (𝑓 ↾
(ℤ≥‘𝑘)) ⊆ 𝑓 |
15 | | dmss 5771 |
. . . . . . . . . . . 12
⊢ ((𝑓 ↾
(ℤ≥‘𝑘)) ⊆ 𝑓 → dom (𝑓 ↾ (ℤ≥‘𝑘)) ⊆ dom 𝑓) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom
(𝑓 ↾
(ℤ≥‘𝑘)) ⊆ dom 𝑓 |
17 | | uzid 12453 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
(ℤ≥‘𝑘)) |
18 | 17 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ (ℤ≥‘𝑘)) |
19 | | fdm 6554 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → dom (𝑓 ↾ (ℤ≥‘𝑘)) =
(ℤ≥‘𝑘)) |
20 | 19 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → dom (𝑓 ↾ (ℤ≥‘𝑘)) =
(ℤ≥‘𝑘)) |
21 | 18, 20 | eleqtrrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ dom (𝑓 ↾ (ℤ≥‘𝑘))) |
22 | 16, 21 | sseldi 3899 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑘 ∈ dom 𝑓) |
23 | 13, 22 | ffvelrnd 6905 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓‘𝑘) ∈ 𝑋) |
24 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘𝐶) =
(MetOpen‘𝐶) |
25 | | eqid 2737 |
. . . . . . . . . . . . 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 23409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) |
30 | 29 | expr 460 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
31 | 30 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
32 | 31 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → ∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟))) |
33 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → 𝑟 ∈ ℝ+) |
34 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓‘𝑘) → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) = ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅))) |
35 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓‘𝑘) → (𝑥(ball‘𝐶)𝑟) = ((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
36 | 34, 35 | sseq12d 3934 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟) ↔ ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
37 | 36 | imbi2d 344 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) ↔ (𝑟 ∈ ℝ+ → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)))) |
38 | 37 | rspcv 3532 |
. . . . . . . . 9
⊢ ((𝑓‘𝑘) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑟 ∈ ℝ+ → (𝑥(ball‘𝐷)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑟)) → (𝑟 ∈ ℝ+ → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)))) |
39 | 23, 32, 33, 38 | syl3c 66 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → ((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) ⊆ ((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
40 | 10, 39 | fssd 6563 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ (𝑘 ∈ ℤ
∧ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)))) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)) |
41 | 40 | expr 460 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
∧ 𝑘 ∈ ℤ)
→ ((𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
42 | 41 | reximdva 3193 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ (∃𝑘 ∈
ℤ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)(𝑟 / 𝑅)) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
43 | 9, 42 | syld 47 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
44 | 43 | ralrimdva 3110 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝑋 ↑pm ℂ)) →
(∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟))) |
45 | 44 | ss2rabdv 3989 |
. 2
⊢ (𝜑 → {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)} ⊆ {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
46 | | metxmet 23232 |
. . 3
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
47 | | caufval 24172 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)}) |
48 | 27, 46, 47 | 3syl 18 |
. 2
⊢ (𝜑 → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑠 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑠)}) |
49 | | metxmet 23232 |
. . 3
⊢ (𝐶 ∈ (Met‘𝑋) → 𝐶 ∈ (∞Met‘𝑋)) |
50 | | caufval 24172 |
. . 3
⊢ (𝐶 ∈ (∞Met‘𝑋) → (Cau‘𝐶) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
51 | 26, 49, 50 | 3syl 18 |
. 2
⊢ (𝜑 → (Cau‘𝐶) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣
∀𝑟 ∈
ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐶)𝑟)}) |
52 | 45, 48, 51 | 3sstr4d 3948 |
1
⊢ (𝜑 → (Cau‘𝐷) ⊆ (Cau‘𝐶)) |