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 = d ∈ V ⟼ x ∈ dom ⁡ dom ⁡ d , z ∈ ℝ * ⟼ y ∈ dom ⁡ dom ⁡ d | x d y < z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbl class ball
1 vd setvar d
2 cvv class V
3 vx setvar x
4 1 cv setvar d
5 4 cdm class dom ⁡ d
6 5 cdm class dom ⁡ dom ⁡ d
7 vz setvar z
8 cxr class ℝ *
9 vy setvar y
10 3 cv setvar x
11 9 cv setvar y
12 10 11 4 co class x d y
13 clt class <
14 7 cv setvar z
15 12 14 13 wbr wff x d y < z
16 15 9 6 crab class y ∈ dom ⁡ dom ⁡ d | x d y < z
17 3 7 6 8 16 cmpo class x ∈ dom ⁡ dom ⁡ d , z ∈ ℝ * ⟼ y ∈ dom ⁡ dom ⁡ d | x d y < z
18 1 2 17 cmpt class d ∈ V ⟼ x ∈ dom ⁡ dom ⁡ d , z ∈ ℝ * ⟼ y ∈ dom ⁡ dom ⁡ d | x d y < z
19 0 18 wceq wff ball = d ∈ V ⟼ x ∈ dom ⁡ dom ⁡ d , z ∈ ℝ * ⟼ y ∈ dom ⁡ dom ⁡ d | x d y < z