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

Metamath Proof Explorer

Definition df-bl

Description: Define the metric space ball function. See blval for its value. (Contributed by NM, 30-Aug-2006) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion df-bl ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbl ⊢ ball
1 vd ⊢ 𝑑
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑑
5 4 cdm ⊢ dom 𝑑
6 5 cdm ⊢ dom dom 𝑑
7 vz ⊢ 𝑧
8 cxr ⊢ ℝ*
9 vy ⊢ 𝑦
10 3 cv ⊢ 𝑥
11 9 cv ⊢ 𝑦
12 10 11 4 co ⊢ ( 𝑥 𝑑 𝑦 )
13 clt ⊢ <
14 7 cv ⊢ 𝑧
15 12 14 13 wbr ⊢ ( 𝑥 𝑑 𝑦 ) < 𝑧
16 15 9 6 crab ⊢ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 }
17 3 7 6 8 16 cmpo ⊢ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } )
18 1 2 17 cmpt ⊢ ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )
19 0 18 wceq ⊢ ball = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ dom dom 𝑑 , 𝑧 ∈ ℝ* ↦ { 𝑦 ∈ dom dom 𝑑 ∣ ( 𝑥 𝑑 𝑦 ) < 𝑧 } ) )