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 \in V ⟼ (x \in dom dom d, z \in ℝ^{*} ⟼ \{y \in 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 \in dom dom d \| x d y < z\}$
17	3 7 6 8 16	cmpo	$class (x \in dom dom d, z \in ℝ^{*} ⟼ \{y \in dom dom d \| x d y < z\})$
18	1 2 17	cmpt	$class (d \in V ⟼ (x \in dom dom d, z \in ℝ^{*} ⟼ \{y \in dom dom d \| x d y < z\}))$
19	0 18	wceq	$wff ball = (d \in V ⟼ (x \in dom dom d, z \in ℝ^{*} ⟼ \{y \in dom dom d \| x d y < z\}))$

Metamath Proof Explorer

Definition df-bl

Detailed syntax breakdown