metustbl

Description: The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017)

		Ref	Expression
	Assertion	metustbl	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to \exists a \in ran ball (D) (P \in a \land a \subseteq V [\{P\}])$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to D \in PsMet (X)$
2		simp3	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to P \in X$
3		simpr	$⊢ (((D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \land w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)])) \land w \subseteq V) \to w \subseteq V$
4		eqid	$⊢ (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) = (r \in ℝ^{+} ⟼ D^{-1} [[0, r)])$
5	4	elrnmpt	$⊢ w \in V \to (w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) \leftrightarrow \exists r \in ℝ^{+} w = D^{-1} [[0, r)])$
6	5	elv	$⊢ w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) \leftrightarrow \exists r \in ℝ^{+} w = D^{-1} [[0, r)]$
7	6	biimpi	$⊢ w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) \to \exists r \in ℝ^{+} w = D^{-1} [[0, r)]$
8	7	ad2antlr	$⊢ (((D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \land w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)])) \land w \subseteq V) \to \exists r \in ℝ^{+} w = D^{-1} [[0, r)]$
9		sseq1	$⊢ w = D^{-1} [[0, r)] \to (w \subseteq V \leftrightarrow D^{-1} [[0, r)] \subseteq V)$
10	9	biimpcd	$⊢ w \subseteq V \to (w = D^{-1} [[0, r)] \to D^{-1} [[0, r)] \subseteq V)$
11	10	reximdv	$⊢ w \subseteq V \to (\exists r \in ℝ^{+} w = D^{-1} [[0, r)] \to \exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V)$
12	3 8 11	sylc	$⊢ (((D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \land w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)])) \land w \subseteq V) \to \exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V$
13	2	ne0d	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to X \neq \emptyset$
14		simp2	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to V \in metUnif (D)$
15		metuel	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in metUnif (D) \leftrightarrow (V \subseteq X \times X \land \exists w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) w \subseteq V))$
16	15	simplbda	$⊢ ((X \neq \emptyset \land D \in PsMet (X)) \land V \in metUnif (D)) \to \exists w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) w \subseteq V$
17	13 1 14 16	syl21anc	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to \exists w \in ran (r \in ℝ^{+} ⟼ D^{-1} [[0, r)]) w \subseteq V$
18	12 17	r19.29a	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to \exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V$
19		imass1	$⊢ D^{-1} [[0, r)] \subseteq V \to D^{-1} [[0, r)] [\{P\}] \subseteq V [\{P\}]$
20	19	reximi	$⊢ \exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V \to \exists r \in ℝ^{+} D^{-1} [[0, r)] [\{P\}] \subseteq V [\{P\}]$
21		blval2	$⊢ (D \in PsMet (X) \land P \in X \land r \in ℝ^{+}) \to P ball (D) r = D^{-1} [[0, r)] [\{P\}]$
22	21	sseq1d	$⊢ (D \in PsMet (X) \land P \in X \land r \in ℝ^{+}) \to (P ball (D) r \subseteq V [\{P\}] \leftrightarrow D^{-1} [[0, r)] [\{P\}] \subseteq V [\{P\}])$
23	22	3expa	$⊢ ((D \in PsMet (X) \land P \in X) \land r \in ℝ^{+}) \to (P ball (D) r \subseteq V [\{P\}] \leftrightarrow D^{-1} [[0, r)] [\{P\}] \subseteq V [\{P\}])$
24	23	rexbidva	$⊢ (D \in PsMet (X) \land P \in X) \to (\exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}] \leftrightarrow \exists r \in ℝ^{+} D^{-1} [[0, r)] [\{P\}] \subseteq V [\{P\}])$
25	20 24	syl5ibr	$⊢ (D \in PsMet (X) \land P \in X) \to (\exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V \to \exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}])$
26	25	imp	$⊢ ((D \in PsMet (X) \land P \in X) \land \exists r \in ℝ^{+} D^{-1} [[0, r)] \subseteq V) \to \exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}]$
27	1 2 18 26	syl21anc	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to \exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}]$
28		blssexps	$⊢ (D \in PsMet (X) \land P \in X) \to (\exists a \in ran ball (D) (P \in a \land a \subseteq V [\{P\}]) \leftrightarrow \exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}])$
29	28	3adant2	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to (\exists a \in ran ball (D) (P \in a \land a \subseteq V [\{P\}]) \leftrightarrow \exists r \in ℝ^{+} P ball (D) r \subseteq V [\{P\}])$
30	27 29	mpbird	$⊢ (D \in PsMet (X) \land V \in metUnif (D) \land P \in X) \to \exists a \in ran ball (D) (P \in a \land a \subseteq V [\{P\}])$

Metamath Proof Explorer

Theorem metustbl

Proof