Metamath Proof Explorer


Theorem blf

Description: Mapping of a ball. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion blf ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )

Proof

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