Metamath Proof Explorer

Theorem psmetutop

Description: The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion psmetutop ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 metuust ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )
2 utopval ⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
3 1 2 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
4 3 eleq2d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑎 ∈ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ) )
5 rabid ⊢ ( 𝑎 ∈ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ↔ ( 𝑎 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
6 4 5 bitrdi ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑎 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) ) )
7 6 biimpa ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ( 𝑎 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
8 7 simpld ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → 𝑎 ∈ 𝒫 𝑋 )
9 8 elpwid ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → 𝑎 ⊆ 𝑋 )
10 unirnblps ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
11 10 ad2antlr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
12 9 11 sseqtrrd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) )
13 simpr ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
14 simp-5r ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
15 simplr ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑣 ∈ ( metUnif ‘ 𝐷 ) )
16 9 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑎 ⊆ 𝑋 )
17 simpllr ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑥 ∈ 𝑎 )
18 16 17 sseldd ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑥 ∈ 𝑋 )
19 metustbl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) ) )
20 14 15 18 19 syl3anc ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) ) )
21 sstr ⊢ ( ( 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → 𝑏 ⊆ 𝑎 )
22 21 expcom ⊢ ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ( 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) → 𝑏 ⊆ 𝑎 ) )
23 22 anim2d ⊢ ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ( ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) ) → ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
24 23 reximdv ⊢ ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑣 “ { 𝑥 } ) ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
25 13 20 24 sylc ⊢ ( ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) ∧ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ) ∧ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) )
26 7 simprd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
27 26 r19.21bi ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
28 25 27 r19.29a ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) )
29 28 ralrimiva ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) )
30 12 29 jca ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ( 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
31 fvex ⊢ ( ball ‘ 𝐷 ) ∈ V
32 31 rnex ⊢ ran ( ball ‘ 𝐷 ) ∈ V
33 eltg2 ⊢ ( ran ( ball ‘ 𝐷 ) ∈ V → ( 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ↔ ( 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) ) )
34 32 33 mp1i ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → ( 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ↔ ( 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) ) )
35 30 34 mpbird ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ) → 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
36 32 33 mp1i ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ↔ ( 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) ) )
37 36 biimpa ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ( 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ) )
38 37 simpld ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → 𝑎 ⊆ ∪ ran ( ball ‘ 𝐷 ) )
39 10 ad2antlr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
40 38 39 sseqtrd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → 𝑎 ⊆ 𝑋 )
41 elpwg ⊢ ( 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) → ( 𝑎 ∈ 𝒫 𝑋 ↔ 𝑎 ⊆ 𝑋 ) )
42 41 adantl ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ( 𝑎 ∈ 𝒫 𝑋 ↔ 𝑎 ⊆ 𝑋 ) )
43 40 42 mpbird ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → 𝑎 ∈ 𝒫 𝑋 )
44 simpllr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
45 40 sselda ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑥 ∈ 𝑋 )
46 37 simprd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) )
47 46 r19.21bi ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) )
48 blssexps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ↔ ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 ) )
49 44 45 48 syl2anc ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑎 ) ↔ ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 ) )
50 47 49 mpbid ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 )
51 blval2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) )
52 51 3expa ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) )
53 52 sseq1d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 ) )
54 53 rexbidva ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 ↔ ∃ 𝑑 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 ) )
55 54 biimpa ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑎 ) → ∃ 𝑑 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 )
56 44 45 50 55 syl21anc ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑑 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 )
57 cnvexg ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V )
58 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V )
59 57 58 syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V )
60 59 ralrimivw ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V )
61 eqid ⊢ ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) = ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) )
62 imaeq1 ⊢ ( 𝑣 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ( 𝑣 “ { 𝑥 } ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) )
63 62 sseq1d ⊢ ( 𝑣 = ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) → ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 ) )
64 61 63 rexrnmptw ⊢ ( ∀ 𝑑 ∈ ℝ+ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ∈ V → ( ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∃ 𝑑 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 ) )
65 44 60 64 3syl ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∃ 𝑑 ∈ ℝ+ ( ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) “ { 𝑥 } ) ⊆ 𝑎 ) )
66 56 65 mpbird ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
67 oveq2 ⊢ ( 𝑑 = 𝑒 → ( 0 [,) 𝑑 ) = ( 0 [,) 𝑒 ) )
68 67 imaeq2d ⊢ ( 𝑑 = 𝑒 → ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
69 68 cbvmptv ⊢ ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) = ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
70 69 rneqi ⊢ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) = ran ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) )
71 70 metustfbas ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
72 ssfg ⊢ ( ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ⊆ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ) )
73 71 72 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ⊆ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ) )
74 metuval ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ) )
75 74 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ) )
76 73 75 sseqtrrd ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ⊆ ( metUnif ‘ 𝐷 ) )
77 ssrexv ⊢ ( ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ⊆ ( metUnif ‘ 𝐷 ) → ( ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
78 76 77 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
79 78 ad2antrr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( ∃ 𝑣 ∈ ran ( 𝑑 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑑 ) ) ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
80 66 79 mpd ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
81 80 ralrimiva ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 )
82 43 81 jca ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → ( 𝑎 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
83 6 biimpar ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ ( metUnif ‘ 𝐷 ) ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) ) → 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) )
84 82 83 syldan ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) → 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) )
85 35 84 impbida ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑎 ∈ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑎 ∈ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) )
86 85 eqrdv ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )