This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blfvalps

Description: The value of the ball function. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion blfvalps ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )

Proof

Step Hyp Ref Expression
1 df-bl ⊢ ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } ) )
2 dmeq ⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
3 2 dmeqd ⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
4 psmetdmdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
5 4 eqcomd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → dom dom 𝐷 = 𝑋 )
6 3 5 sylan9eqr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
7 eqidd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ℝ* = ℝ* )
8 simpr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
9 8 oveqd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
10 9 breq1d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 𝑑 𝑦 ) < 𝑟 ↔ ( 𝑥 𝐷 𝑦 ) < 𝑟 ) )
11 6 10 rabeqbidv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } = { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } )
12 6 7 11 mpoeq123dv ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ dom dom 𝑑 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑟 } ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )
13 elex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ V )
14 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋
15 elfvdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet )
16 15 adantr ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → 𝑋 ∈ dom PsMet )
17 elpw2g ⊢ ( 𝑋 ∈ dom PsMet → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) )
18 16 17 syl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → ( { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ⊆ 𝑋 ) )
19 14 18 mpbiri ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 )
20 19 ralrimivva ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 )
21 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } )
22 21 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ* { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ∈ 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
23 20 22 sylib ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
24 xrex ⊢ ℝ* ∈ V
25 xpexg ⊢ ( ( 𝑋 ∈ dom PsMet ∧ ℝ* ∈ V ) → ( 𝑋 × ℝ* ) ∈ V )
26 15 24 25 sylancl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑋 × ℝ* ) ∈ V )
27 15 pwexd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝒫 𝑋 ∈ V )
28 fex2 ⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ∧ ( 𝑋 × ℝ* ) ∈ V ∧ 𝒫 𝑋 ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) ∈ V )
29 23 26 27 28 syl3anc ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) ∈ V )
30 1 12 13 29 fvmptd2 ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑥 ∈ 𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑦 ∈ 𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < 𝑟 } ) )