Step | Hyp | Ref
| Expression |
1 | | equivtotbnd.2 |
. 2
⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) |
2 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
3 | | equivtotbnd.3 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑅 ∈
ℝ+) |
5 | 2, 4 | rpdivcld 12734 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 𝑅) ∈
ℝ+) |
6 | | equivtotbnd.1 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (TotBnd‘𝑋)) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑀 ∈ (TotBnd‘𝑋)) |
8 | | istotbnd3 35898 |
. . . . . . 7
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑠 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋)) |
9 | 8 | simprbi 496 |
. . . . . 6
⊢ (𝑀 ∈ (TotBnd‘𝑋) → ∀𝑠 ∈ ℝ+
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋) |
10 | 7, 9 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑠 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋) |
11 | | oveq2 7268 |
. . . . . . . . 9
⊢ (𝑠 = (𝑟 / 𝑅) → (𝑥(ball‘𝑀)𝑠) = (𝑥(ball‘𝑀)(𝑟 / 𝑅))) |
12 | 11 | iuneq2d 4955 |
. . . . . . . 8
⊢ (𝑠 = (𝑟 / 𝑅) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅))) |
13 | 12 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑠 = (𝑟 / 𝑅) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 ↔ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) |
14 | 13 | rexbidv 3224 |
. . . . . 6
⊢ (𝑠 = (𝑟 / 𝑅) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) |
15 | 14 | rspcv 3552 |
. . . . 5
⊢ ((𝑟 / 𝑅) ∈ ℝ+ →
(∀𝑠 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) |
16 | 5, 10, 15 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋) |
17 | | elfpw 9067 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin)) |
18 | 17 | simplbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋) |
19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑣 ⊆ 𝑋) |
20 | 19 | sselda 3922 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑋) |
21 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘𝑁) =
(MetOpen‘𝑁) |
22 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘𝑀) =
(MetOpen‘𝑀) |
23 | 8 | simplbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) |
24 | 6, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) |
25 | | equivtotbnd.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) |
26 | 21, 22, 1, 24, 3, 25 | metss2lem 23611 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) |
27 | 26 | anass1rs 651 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) |
28 | 27 | adantlr 711 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) |
29 | 20, 28 | syldan 590 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) |
30 | 29 | ralrimiva 3106 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) |
31 | | ss2iun 4944 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)) |
33 | | sseq1 3947 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ↔ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) |
34 | 32, 33 | syl5ibcom 244 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) |
35 | 1 | ad3antrrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑁 ∈ (Met‘𝑋)) |
36 | | metxmet 23431 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (Met‘𝑋) → 𝑁 ∈ (∞Met‘𝑋)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑁 ∈ (∞Met‘𝑋)) |
38 | | simpllr 772 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑟 ∈ ℝ+) |
39 | 38 | rpxrd 12718 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑟 ∈ ℝ*) |
40 | | blssm 23515 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) |
41 | 37, 20, 39, 40 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) |
42 | 41 | ralrimiva 3106 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) |
43 | | iunss 4976 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) |
44 | 42, 43 | sylibr 233 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) |
45 | 34, 44 | jctild 525 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)))) |
46 | | eqss 3937 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋 ↔ (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) |
47 | 45, 46 | syl6ibr 251 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) |
48 | 47 | reximdva 3201 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) |
49 | 16, 48 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋) |
50 | 49 | ralrimiva 3106 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋) |
51 | | istotbnd3 35898 |
. 2
⊢ (𝑁 ∈ (TotBnd‘𝑋) ↔ (𝑁 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) |
52 | 1, 50, 51 | sylanbrc 582 |
1
⊢ (𝜑 → 𝑁 ∈ (TotBnd‘𝑋)) |