| 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 13095 | . . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 𝑅) ∈
ℝ+) | 
| 6 |  | equivtotbnd.1 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (TotBnd‘𝑋)) | 
| 7 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑀 ∈ (TotBnd‘𝑋)) | 
| 8 |  | istotbnd3 37779 | . . . . . . 7
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑠 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋)) | 
| 9 | 8 | simprbi 496 | . . . . . 6
⊢ (𝑀 ∈ (TotBnd‘𝑋) → ∀𝑠 ∈ ℝ+
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋) | 
| 10 | 7, 9 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑠 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋) | 
| 11 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑠 = (𝑟 / 𝑅) → (𝑥(ball‘𝑀)𝑠) = (𝑥(ball‘𝑀)(𝑟 / 𝑅))) | 
| 12 | 11 | iuneq2d 5021 | . . . . . . . 8
⊢ (𝑠 = (𝑟 / 𝑅) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅))) | 
| 13 | 12 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑠 = (𝑟 / 𝑅) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 ↔ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) | 
| 14 | 13 | rexbidv 3178 | . . . . . 6
⊢ (𝑠 = (𝑟 / 𝑅) → (∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 ↔ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) | 
| 15 | 14 | rspcv 3617 | . . . . 5
⊢ ((𝑟 / 𝑅) ∈ ℝ+ →
(∀𝑠 ∈
ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑠) = 𝑋 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋)) | 
| 16 | 5, 10, 15 | sylc 65 | . . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋) | 
| 17 |  | elfpw 9395 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) ↔ (𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin)) | 
| 18 | 17 | simplbi 497 | . . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝒫 𝑋 ∩ Fin) → 𝑣 ⊆ 𝑋) | 
| 19 | 18 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑣 ⊆ 𝑋) | 
| 20 | 19 | sselda 3982 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑋) | 
| 21 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(MetOpen‘𝑁) =
(MetOpen‘𝑁) | 
| 22 |  | eqid 2736 | . . . . . . . . . . . . . 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 24525 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) | 
| 27 | 26 | anass1rs 655 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) | 
| 28 | 27 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) | 
| 29 | 20, 28 | syldan 591 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) | 
| 30 | 29 | ralrimiva 3145 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟)) | 
| 31 |  | ss2iun 5009 | . . . . . . . . 9
⊢
(∀𝑥 ∈
𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ (𝑥(ball‘𝑁)𝑟) → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)) | 
| 32 | 30, 31 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)) | 
| 33 |  | sseq1 4008 | . . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ↔ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) | 
| 34 | 32, 33 | syl5ibcom 245 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) | 
| 35 | 1 | ad3antrrr 730 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑁 ∈ (Met‘𝑋)) | 
| 36 |  | metxmet 24345 | . . . . . . . . . . 11
⊢ (𝑁 ∈ (Met‘𝑋) → 𝑁 ∈ (∞Met‘𝑋)) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑁 ∈ (∞Met‘𝑋)) | 
| 38 |  | simpllr 775 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑟 ∈ ℝ+) | 
| 39 | 38 | rpxrd 13079 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → 𝑟 ∈ ℝ*) | 
| 40 |  | blssm 24429 | . . . . . . . . . 10
⊢ ((𝑁 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) | 
| 41 | 37, 20, 39, 40 | syl3anc 1372 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑣) → (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) | 
| 42 | 41 | ralrimiva 3145 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) →
∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) | 
| 43 |  | iunss 5044 | . . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ↔ ∀𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) | 
| 44 | 42, 43 | sylibr 234 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋) | 
| 45 | 34, 44 | jctild 525 | . . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟)))) | 
| 46 |  | eqss 3998 | . . . . . 6
⊢ (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋 ↔ (∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟))) | 
| 47 | 45, 46 | imbitrrdi 252 | . . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑣 ∈ (𝒫 𝑋 ∩ Fin)) → (∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → ∪
𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) | 
| 48 | 47 | reximdva 3167 | . . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)(𝑟 / 𝑅)) = 𝑋 → ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) | 
| 49 | 16, 48 | mpd 15 | . . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑣 ∈ (𝒫
𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋) | 
| 50 | 49 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋) | 
| 51 |  | istotbnd3 37779 | . 2
⊢ (𝑁 ∈ (TotBnd‘𝑋) ↔ (𝑁 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑁)𝑟) = 𝑋)) | 
| 52 | 1, 50, 51 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑁 ∈ (TotBnd‘𝑋)) |