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 ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )