blf

Description: Mapping of a ball. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	blf	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{y \in X \| x D y < r\} \subseteq X$
2		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
3		elpw2g	$⊢ X \in dom ∞Met \to (\{y \in X \| x D y < r\} \in 𝒫 X \leftrightarrow \{y \in X \| x D y < r\} \subseteq X)$
4	2 3	syl	$⊢ D \in ∞Met (X) \to (\{y \in X \| x D y < r\} \in 𝒫 X \leftrightarrow \{y \in X \| x D y < r\} \subseteq X)$
5	1 4	mpbiri	$⊢ D \in ∞Met (X) \to \{y \in X \| x D y < r\} \in 𝒫 X$
6	5	a1d	$⊢ D \in ∞Met (X) \to ((x \in X \land r \in ℝ^{*}) \to \{y \in X \| x D y < r\} \in 𝒫 X)$
7	6	ralrimivv	$⊢ D \in ∞Met (X) \to \forall x \in X \forall r \in ℝ^{*} \{y \in X \| x D y < r\} \in 𝒫 X$
8		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\})$
9	8	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$
10	7 9	sylib	$⊢ D \in ∞Met (X) \to (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) : X \times ℝ^{} ⟶ 𝒫 X$
11		blfval	$⊢ D \in ∞Met (X) \to ball (D) = (x \in X, r \in ℝ^{*} ⟼ \{y \in X \| x D y < r\})$
12	11	feq1d	$⊢ D \in ∞Met (X) \to (ball (D) : X \times ℝ^{} ⟶ 𝒫 X \leftrightarrow (x \in X, r \in ℝ^{} ⟼ \{y \in X \| x D y < r\}) : X \times ℝ^{*} ⟶ 𝒫 X)$
13	10 12	mpbird	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$

Metamath Proof Explorer