| Step | Hyp | Ref
| Expression |
| 1 | | metuust 24573 |
. . . . . . . . . . . 12
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) ∈ (UnifOn‘𝑋)) |
| 2 | | utopval 24241 |
. . . . . . . . . . . 12
⊢
((metUnif‘𝐷)
∈ (UnifOn‘𝑋)
→ (unifTop‘(metUnif‘𝐷)) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎}) |
| 3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) →
(unifTop‘(metUnif‘𝐷)) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎}) |
| 4 | 3 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑎 ∈ (unifTop‘(metUnif‘𝐷)) ↔ 𝑎 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎})) |
| 5 | | rabid 3458 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎} ↔ (𝑎 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 6 | 4, 5 | bitrdi 287 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑎 ∈ (unifTop‘(metUnif‘𝐷)) ↔ (𝑎 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎))) |
| 7 | 6 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → (𝑎 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 8 | 7 | simpld 494 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → 𝑎 ∈ 𝒫 𝑋) |
| 9 | 8 | elpwid 4609 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → 𝑎 ⊆ 𝑋) |
| 10 | | unirnblps 24429 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∪ ran (ball‘𝐷) = 𝑋) |
| 11 | 10 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → ∪ ran (ball‘𝐷) = 𝑋) |
| 12 | 9, 11 | sseqtrrd 4021 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → 𝑎 ⊆ ∪ ran
(ball‘𝐷)) |
| 13 | | simpr 484 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → (𝑣 “ {𝑥}) ⊆ 𝑎) |
| 14 | | simp-5r 786 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝐷 ∈ (PsMet‘𝑋)) |
| 15 | | simplr 769 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝑣 ∈ (metUnif‘𝐷)) |
| 16 | 9 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋) |
| 17 | | simpllr 776 |
. . . . . . . . . 10
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝑥 ∈ 𝑎) |
| 18 | 16, 17 | sseldd 3984 |
. . . . . . . . 9
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝑥 ∈ 𝑋) |
| 19 | | metustbl 24579 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑣 ∈ (metUnif‘𝐷) ∧ 𝑥 ∈ 𝑋) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑣 “ {𝑥}))) |
| 20 | 14, 15, 18, 19 | syl3anc 1373 |
. . . . . . . 8
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑣 “ {𝑥}))) |
| 21 | | sstr 3992 |
. . . . . . . . . . 11
⊢ ((𝑏 ⊆ (𝑣 “ {𝑥}) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → 𝑏 ⊆ 𝑎) |
| 22 | 21 | expcom 413 |
. . . . . . . . . 10
⊢ ((𝑣 “ {𝑥}) ⊆ 𝑎 → (𝑏 ⊆ (𝑣 “ {𝑥}) → 𝑏 ⊆ 𝑎)) |
| 23 | 22 | anim2d 612 |
. . . . . . . . 9
⊢ ((𝑣 “ {𝑥}) ⊆ 𝑎 → ((𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑣 “ {𝑥})) → (𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎))) |
| 24 | 23 | reximdv 3170 |
. . . . . . . 8
⊢ ((𝑣 “ {𝑥}) ⊆ 𝑎 → (∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑣 “ {𝑥})) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎))) |
| 25 | 13, 20, 24 | sylc 65 |
. . . . . . 7
⊢
((((((𝑋 ≠ ∅
∧ 𝐷 ∈
(PsMet‘𝑋)) ∧
𝑎 ∈
(unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) ∧ 𝑣 ∈ (metUnif‘𝐷)) ∧ (𝑣 “ {𝑥}) ⊆ 𝑎) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)) |
| 26 | 7 | simprd 495 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎) |
| 27 | 26 | r19.21bi 3251 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎) |
| 28 | 25, 27 | r19.29a 3162 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)) |
| 29 | 28 | ralrimiva 3146 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → ∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)) |
| 30 | 12, 29 | jca 511 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → (𝑎 ⊆ ∪ ran
(ball‘𝐷) ∧
∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎))) |
| 31 | | fvex 6919 |
. . . . . 6
⊢
(ball‘𝐷)
∈ V |
| 32 | 31 | rnex 7932 |
. . . . 5
⊢ ran
(ball‘𝐷) ∈
V |
| 33 | | eltg2 22965 |
. . . . 5
⊢ (ran
(ball‘𝐷) ∈ V
→ (𝑎 ∈
(topGen‘ran (ball‘𝐷)) ↔ (𝑎 ⊆ ∪ ran
(ball‘𝐷) ∧
∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)))) |
| 34 | 32, 33 | mp1i 13 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → (𝑎 ∈ (topGen‘ran (ball‘𝐷)) ↔ (𝑎 ⊆ ∪ ran
(ball‘𝐷) ∧
∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)))) |
| 35 | 30, 34 | mpbird 257 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) → 𝑎 ∈ (topGen‘ran (ball‘𝐷))) |
| 36 | 32, 33 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑎 ∈ (topGen‘ran (ball‘𝐷)) ↔ (𝑎 ⊆ ∪ ran
(ball‘𝐷) ∧
∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)))) |
| 37 | 36 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → (𝑎 ⊆ ∪ ran
(ball‘𝐷) ∧
∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎))) |
| 38 | 37 | simpld 494 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → 𝑎 ⊆ ∪ ran
(ball‘𝐷)) |
| 39 | 10 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → ∪ ran (ball‘𝐷) = 𝑋) |
| 40 | 38, 39 | sseqtrd 4020 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → 𝑎 ⊆ 𝑋) |
| 41 | | elpwg 4603 |
. . . . . . 7
⊢ (𝑎 ∈ (topGen‘ran
(ball‘𝐷)) →
(𝑎 ∈ 𝒫 𝑋 ↔ 𝑎 ⊆ 𝑋)) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → (𝑎 ∈ 𝒫 𝑋 ↔ 𝑎 ⊆ 𝑋)) |
| 43 | 40, 42 | mpbird 257 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → 𝑎 ∈ 𝒫 𝑋) |
| 44 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → 𝐷 ∈ (PsMet‘𝑋)) |
| 45 | 40 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑋) |
| 46 | 37 | simprd 495 |
. . . . . . . . . . 11
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → ∀𝑥 ∈ 𝑎 ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)) |
| 47 | 46 | r19.21bi 3251 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎)) |
| 48 | | blssexps 24436 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑑 ∈ ℝ+ (𝑥(ball‘𝐷)𝑑) ⊆ 𝑎)) |
| 49 | 44, 45, 48 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → (∃𝑏 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎) ↔ ∃𝑑 ∈ ℝ+ (𝑥(ball‘𝐷)𝑑) ⊆ 𝑎)) |
| 50 | 47, 49 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑑 ∈ ℝ+ (𝑥(ball‘𝐷)𝑑) ⊆ 𝑎) |
| 51 | | blval2 24575 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ ℝ+) → (𝑥(ball‘𝐷)𝑑) = ((◡𝐷 “ (0[,)𝑑)) “ {𝑥})) |
| 52 | 51 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑑 ∈ ℝ+) → (𝑥(ball‘𝐷)𝑑) = ((◡𝐷 “ (0[,)𝑑)) “ {𝑥})) |
| 53 | 52 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑑 ∈ ℝ+) → ((𝑥(ball‘𝐷)𝑑) ⊆ 𝑎 ↔ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎)) |
| 54 | 53 | rexbidva 3177 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) → (∃𝑑 ∈ ℝ+ (𝑥(ball‘𝐷)𝑑) ⊆ 𝑎 ↔ ∃𝑑 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎)) |
| 55 | 54 | biimpa 476 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ ∃𝑑 ∈ ℝ+ (𝑥(ball‘𝐷)𝑑) ⊆ 𝑎) → ∃𝑑 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎) |
| 56 | 44, 45, 50, 55 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑑 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎) |
| 57 | | cnvexg 7946 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (PsMet‘𝑋) → ◡𝐷 ∈ V) |
| 58 | | imaexg 7935 |
. . . . . . . . . . 11
⊢ (◡𝐷 ∈ V → (◡𝐷 “ (0[,)𝑑)) ∈ V) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (PsMet‘𝑋) → (◡𝐷 “ (0[,)𝑑)) ∈ V) |
| 60 | 59 | ralrimivw 3150 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∀𝑑 ∈ ℝ+
(◡𝐷 “ (0[,)𝑑)) ∈ V) |
| 61 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑑 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑑))) = (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) |
| 62 | | imaeq1 6073 |
. . . . . . . . . . 11
⊢ (𝑣 = (◡𝐷 “ (0[,)𝑑)) → (𝑣 “ {𝑥}) = ((◡𝐷 “ (0[,)𝑑)) “ {𝑥})) |
| 63 | 62 | sseq1d 4015 |
. . . . . . . . . 10
⊢ (𝑣 = (◡𝐷 “ (0[,)𝑑)) → ((𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎)) |
| 64 | 61, 63 | rexrnmptw 7115 |
. . . . . . . . 9
⊢
(∀𝑑 ∈
ℝ+ (◡𝐷 “ (0[,)𝑑)) ∈ V → (∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∃𝑑 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎)) |
| 65 | 44, 60, 64 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → (∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∃𝑑 ∈ ℝ+ ((◡𝐷 “ (0[,)𝑑)) “ {𝑥}) ⊆ 𝑎)) |
| 66 | 56, 65 | mpbird 257 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎) |
| 67 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑒 → (0[,)𝑑) = (0[,)𝑒)) |
| 68 | 67 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑒 → (◡𝐷 “ (0[,)𝑑)) = (◡𝐷 “ (0[,)𝑒))) |
| 69 | 68 | cbvmptv 5255 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑑))) = (𝑒 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑒))) |
| 70 | 69 | rneqi 5948 |
. . . . . . . . . . . 12
⊢ ran
(𝑑 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) = ran (𝑒 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑒))) |
| 71 | 70 | metustfbas 24570 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑑 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑑))) ∈ (fBas‘(𝑋 × 𝑋))) |
| 72 | | ssfg 23880 |
. . . . . . . . . . 11
⊢ (ran
(𝑑 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) ∈ (fBas‘(𝑋 × 𝑋)) → ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) ⊆ ((𝑋 × 𝑋)filGenran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))))) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑑 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑑))) ⊆ ((𝑋 × 𝑋)filGenran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))))) |
| 74 | | metuval 24562 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))))) |
| 75 | 74 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))))) |
| 76 | 73, 75 | sseqtrrd 4021 |
. . . . . . . . 9
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ran (𝑑 ∈ ℝ+
↦ (◡𝐷 “ (0[,)𝑑))) ⊆ (metUnif‘𝐷)) |
| 77 | | ssrexv 4053 |
. . . . . . . . 9
⊢ (ran
(𝑑 ∈
ℝ+ ↦ (◡𝐷 “ (0[,)𝑑))) ⊆ (metUnif‘𝐷) → (∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎 → ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 78 | 76, 77 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎 → ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 79 | 78 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → (∃𝑣 ∈ ran (𝑑 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑑)))(𝑣 “ {𝑥}) ⊆ 𝑎 → ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 80 | 66, 79 | mpd 15 |
. . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) ∧ 𝑥 ∈ 𝑎) → ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎) |
| 81 | 80 | ralrimiva 3146 |
. . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎) |
| 82 | 43, 81 | jca 511 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → (𝑎 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) |
| 83 | 6 | biimpar 477 |
. . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ (𝑎 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ (metUnif‘𝐷)(𝑣 “ {𝑥}) ⊆ 𝑎)) → 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) |
| 84 | 82, 83 | syldan 591 |
. . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝑎 ∈ (topGen‘ran (ball‘𝐷))) → 𝑎 ∈ (unifTop‘(metUnif‘𝐷))) |
| 85 | 35, 84 | impbida 801 |
. 2
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑎 ∈ (unifTop‘(metUnif‘𝐷)) ↔ 𝑎 ∈ (topGen‘ran (ball‘𝐷)))) |
| 86 | 85 | eqrdv 2735 |
1
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) →
(unifTop‘(metUnif‘𝐷)) = (topGen‘ran (ball‘𝐷))) |