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 β€˜ 𝐷 ) : ( 𝑋 Γ— ℝ* ) ⟢ 𝒫 𝑋 )