Step |
Hyp |
Ref |
Expression |
1 |
|
metuval |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) |
2 |
1
|
adantl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) |
3 |
2
|
eleq2d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) ) |
4 |
|
oveq2 |
⊢ ( 𝑎 = 𝑒 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑒 ) ) |
5 |
4
|
imaeq2d |
⊢ ( 𝑎 = 𝑒 → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) ) |
6 |
5
|
cbvmptv |
⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) ) |
7 |
6
|
rneqi |
⊢ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑒 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑒 ) ) ) |
8 |
7
|
metustfbas |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ) |
9 |
|
elfg |
⊢ ( ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) ) |
11 |
3 10
|
bitrd |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑉 ∈ ( metUnif ‘ 𝐷 ) ↔ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑤 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) 𝑤 ⊆ 𝑉 ) ) ) |