Step |
Hyp |
Ref |
Expression |
1 |
|
metust.1 |
⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) |
2 |
1
|
eleq2i |
⊢ ( 𝐵 ∈ 𝐹 ↔ 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) |
3 |
|
elex |
⊢ ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐵 ∈ V ) |
4 |
3
|
a1i |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) → 𝐵 ∈ V ) ) |
5 |
|
cnvexg |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ◡ 𝐷 ∈ V ) |
6 |
|
imaexg |
⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V ) |
7 |
|
eleq1a |
⊢ ( ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ∈ V → ( 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) ) |
8 |
5 6 7
|
3syl |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) ) |
9 |
8
|
rexlimdvw |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) → 𝐵 ∈ V ) ) |
10 |
|
eqid |
⊢ ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) |
11 |
10
|
elrnmpt |
⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) |
12 |
11
|
a1i |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ V → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) |
13 |
4 9 12
|
pm5.21ndd |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) |
14 |
2 13
|
syl5bb |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝐵 ∈ 𝐹 ↔ ∃ 𝑎 ∈ ℝ+ 𝐵 = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) |