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	$⊢ D \in PsMet (X) \to ball (D) = (x \in X, r \in ℝ^{*} ⟼ \{y \in X \| x D y < r\})$

Proof

Step	Hyp	Ref	Expression
1		df-bl	$⊢ ball = (d \in V ⟼ (x \in dom dom d, r \in ℝ^{*} ⟼ \{y \in dom dom d \| x d y < r\}))$
2		dmeq	$⊢ d = D \to dom d = dom D$
3	2	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
4		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
5	4	eqcomd	$⊢ D \in PsMet (X) \to dom dom D = X$
6	3 5	sylan9eqr	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = X$
7		eqidd	$⊢ (D \in PsMet (X) \land d = D) \to ℝ^{} = ℝ^{}$
8		simpr	$⊢ (D \in PsMet (X) \land d = D) \to d = D$
9	8	oveqd	$⊢ (D \in PsMet (X) \land d = D) \to x d y = x D y$
10	9	breq1d	$⊢ (D \in PsMet (X) \land d = D) \to (x d y < r \leftrightarrow x D y < r)$
11	6 10	rabeqbidv	$⊢ (D \in PsMet (X) \land d = D) \to \{y \in dom dom d \| x d y < r\} = \{y \in X \| x D y < r\}$
12	6 7 11	mpoeq123dv	$⊢ (D \in PsMet (X) \land d = D) \to (x \in dom dom d, r \in ℝ^{} ⟼ \{y \in dom dom d \| x d y < r\}) = (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\})$
13		elex	$⊢ D \in PsMet (X) \to D \in V$
14		ssrab2	$⊢ \{y \in X \| x D y < r\} \subseteq X$
15		elfvdm	$⊢ D \in PsMet (X) \to X \in dom PsMet$
16	15	adantr	$⊢ (D \in PsMet (X) \land (x \in X \land r \in ℝ^{*})) \to X \in dom PsMet$
17		elpw2g	$⊢ X \in dom PsMet \to (\{y \in X \| x D y < r\} \in 𝒫 X \leftrightarrow \{y \in X \| x D y < r\} \subseteq X)$
18	16 17	syl	$⊢ (D \in PsMet (X) \land (x \in X \land r \in ℝ^{*})) \to (\{y \in X \| x D y < r\} \in 𝒫 X \leftrightarrow \{y \in X \| x D y < r\} \subseteq X)$
19	14 18	mpbiri	$⊢ (D \in PsMet (X) \land (x \in X \land r \in ℝ^{*})) \to \{y \in X \| x D y < r\} \in 𝒫 X$
20	19	ralrimivva	$⊢ D \in PsMet (X) \to \forall x \in X \forall r \in ℝ^{*} \{y \in X \| x D y < r\} \in 𝒫 X$
21		eqid	$⊢ (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) = (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\})$
22	21	fmpo	$⊢ \forall x \in X \forall r \in ℝ^{} \{y \in X \| x D y < r\} \in 𝒫 X \leftrightarrow (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) : X \times ℝ^{*} ⟶ 𝒫 X$
23	20 22	sylib	$⊢ D \in PsMet (X) \to (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) : X \times ℝ^{} ⟶ 𝒫 X$
24		xrex	$⊢ ℝ^{*} \in V$
25		xpexg	$⊢ (X \in dom PsMet \land ℝ^{} \in V) \to X \times ℝ^{} \in V$
26	15 24 25	sylancl	$⊢ D \in PsMet (X) \to X \times ℝ^{*} \in V$
27	15	pwexd	$⊢ D \in PsMet (X) \to 𝒫 X \in V$
28		fex2	$⊢ ((x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) : X \times ℝ^{} ⟶ 𝒫 X \land X \times ℝ^{} \in V \land 𝒫 X \in V) \to (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) \in V$
29	23 26 27 28	syl3anc	$⊢ D \in PsMet (X) \to (x \in X, r \in ℝ^{*} ⟼ \{y \in X \| x D y < r\}) \in V$
30	1 12 13 29	fvmptd2	$⊢ D \in PsMet (X) \to ball (D) = (x \in X, r \in ℝ^{*} ⟼ \{y \in X \| x D y < r\})$

Metamath Proof Explorer

Theorem blfvalps

Proof