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

Metamath Proof Explorer

Theorem tusunif

Description: The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

		Ref	Expression
	Hypothesis	tuslem.k	$⊢ K = toUnifSp (U)$
	Assertion	tusunif	$⊢ U \in UnifOn (X) \to U = UnifSet (K)$

Step	Hyp	Ref	Expression
1		tuslem.k	$⊢ K = toUnifSp (U)$
2	1	tuslem	$⊢ U \in UnifOn (X) \to (X = {Base}_{K} \land U = UnifSet (K) \land unifTop (U) = TopOpen (K))$
3	2	simp2d	$⊢ U \in UnifOn (X) \to U = UnifSet (K)$