isbndx

Description: A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	isbndx	$⊢ M \in Bnd (X) \leftrightarrow (M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$

Proof

Step	Hyp	Ref	Expression
1		isbnd	$⊢ M \in Bnd (X) \leftrightarrow (M \in Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
2		metxmet	$⊢ M \in Met (X) \to M \in ∞Met (X)$
3		simpr	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land M \in ∞Met (X)) \to M \in ∞Met (X)$
4		xmetf	$⊢ M \in ∞Met (X) \to M : X \times X ⟶ ℝ^{*}$
5		ffn	$⊢ M : X \times X ⟶ ℝ^{*} \to M Fn (X \times X)$
6	3 4 5	3syl	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land M \in ∞Met (X)) \to M Fn (X \times X)$
7		simprr	$⊢ ((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \to X = x ball (M) r$
8		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
9		eqid	$⊢ M^{-1} [ℝ] = M^{-1} [ℝ]$
10	9	blssec	$⊢ (M \in ∞Met (X) \land x \in X \land r \in ℝ^{*}) \to x ball (M) r \subseteq [x] M^{-1} [ℝ]$
11	10	3expa	$⊢ ((M \in ∞Met (X) \land x \in X) \land r \in ℝ^{*}) \to x ball (M) r \subseteq [x] M^{-1} [ℝ]$
12	8 11	sylan2	$⊢ ((M \in ∞Met (X) \land x \in X) \land r \in ℝ^{+}) \to x ball (M) r \subseteq [x] M^{-1} [ℝ]$
13	12	adantrr	$⊢ ((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \to x ball (M) r \subseteq [x] M^{-1} [ℝ]$
14	7 13	eqsstrd	$⊢ ((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \to X \subseteq [x] M^{-1} [ℝ]$
15	14	sselda	$⊢ (((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \land y \in X) \to y \in [x] M^{-1} [ℝ]$
16		vex	$⊢ y \in V$
17		vex	$⊢ x \in V$
18	16 17	elec	$⊢ y \in [x] M^{-1} [ℝ] \leftrightarrow x M^{-1} [ℝ] y$
19	15 18	sylib	$⊢ (((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \land y \in X) \to x M^{-1} [ℝ] y$
20	9	xmeterval	$⊢ M \in ∞Met (X) \to (x M^{-1} [ℝ] y \leftrightarrow (x \in X \land y \in X \land x M y \in ℝ))$
21	20	ad3antrrr	$⊢ (((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \land y \in X) \to (x M^{-1} [ℝ] y \leftrightarrow (x \in X \land y \in X \land x M y \in ℝ))$
22	19 21	mpbid	$⊢ (((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \land y \in X) \to (x \in X \land y \in X \land x M y \in ℝ)$
23	22	simp3d	$⊢ (((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \land y \in X) \to x M y \in ℝ$
24	23	ralrimiva	$⊢ ((M \in ∞Met (X) \land x \in X) \land (r \in ℝ^{+} \land X = x ball (M) r)) \to \forall y \in X x M y \in ℝ$
25	24	rexlimdvaa	$⊢ (M \in ∞Met (X) \land x \in X) \to (\exists r \in ℝ^{+} X = x ball (M) r \to \forall y \in X x M y \in ℝ)$
26	25	ralimdva	$⊢ M \in ∞Met (X) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \forall x \in X \forall y \in X x M y \in ℝ)$
27	26	impcom	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land M \in ∞Met (X)) \to \forall x \in X \forall y \in X x M y \in ℝ$
28		ffnov	$⊢ M : X \times X ⟶ ℝ \leftrightarrow (M Fn (X \times X) \land \forall x \in X \forall y \in X x M y \in ℝ)$
29	6 27 28	sylanbrc	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land M \in ∞Met (X)) \to M : X \times X ⟶ ℝ$
30		ismet2	$⊢ M \in Met (X) \leftrightarrow (M \in ∞Met (X) \land M : X \times X ⟶ ℝ)$
31	3 29 30	sylanbrc	$⊢ (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \land M \in ∞Met (X)) \to M \in Met (X)$
32	31	ex	$⊢ \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (M \in ∞Met (X) \to M \in Met (X))$
33	2 32	impbid2	$⊢ \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (M \in Met (X) \leftrightarrow M \in ∞Met (X))$
34	33	pm5.32ri	$⊢ (M \in Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r) \leftrightarrow (M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
35	1 34	bitri	$⊢ M \in Bnd (X) \leftrightarrow (M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$

Metamath Proof Explorer

Theorem isbndx

Proof