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

Metamath Proof Explorer

Theorem tusbas

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

		Ref	Expression
	Hypothesis	tuslem.k	$⊢ K = toUnifSp (U)$
	Assertion	tusbas	$⊢ U \in UnifOn (X) \to X = {Base}_{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	simp1d	$⊢ U \in UnifOn (X) \to X = {Base}_{K}$