Metamath Proof Explorer

Theorem metuust

Description: The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	metuust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) \in UnifOn (X)$

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		oveq2	$⊢ a = b \to [0, a) = [0, b)$
4	3	imaeq2d	$⊢ a = b \to D^{-1} [[0, a)] = D^{-1} [[0, b)]$
5	4	cbvmptv	$⊢ (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
6	5	rneqi	$⊢ ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) = ran (b \in ℝ^{+} ⟼ D^{-1} [[0, b)])$
7	6	metust	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \in UnifOn (X)$
8	2 7	eqeltrd	$⊢ (X \neq \emptyset \land D \in PsMet (X)) \to metUnif (D) \in UnifOn (X)$