Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
⊢ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 |
2 |
|
elfvdm |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet ) |
3 |
|
elpw2g |
⊢ ( 𝑋 ∈ dom PsMet → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) ) |
4 |
2 3
|
syl |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) ) |
5 |
1 4
|
mpbiri |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ) |
6 |
5
|
a1d |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ) ) |
7 |
6
|
ralrimivv |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ) |
8 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) |
9 |
8
|
fmpo |
⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ) |
10 |
7 9
|
sylib |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ) |
11 |
|
blfvalps |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) ) |
12 |
11
|
feq1d |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ) ) |
13 |
10 12
|
mpbird |
⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ) |