This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metuel

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	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 (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V))$

Proof

Step	Hyp	Ref	Expression
1		metuval	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
2	1	adantl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
3	2	eleq2d	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in metUnif (D) \leftrightarrow V \in ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])))$
4		oveq2	$⊢ a = e \to [0, a) = [0, e)$
5	4	imaeq2d	$⊢ a = e \to D^{-1} [[0, a)] = D^{-1} [[0, e)]$
6	5	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (e \in ℝ^{+} ⟼ D^{-1} [[0, e)])$
7	6	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = ran (e \in ℝ^{+} ⟼ D^{-1} [[0, e)])$
8	7	metustfbas	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \in fBas (X \times X)$
9		elfg	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \in fBas (X \times X) \to (V \in ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \leftrightarrow (V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V))$
10	8 9	syl	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in ((X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])) \leftrightarrow (V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V))$
11	3 10	bitrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (V \in metUnif (D) \leftrightarrow (V \subseteq X \times X \land \exists w \in ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) w \subseteq V))$