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 UnifOn X U = UnifSet K

Proof

Step Hyp Ref Expression
1 tuslem.k K = toUnifSp U
2 1 tuslem U UnifOn X X = Base K U = UnifSet K unifTop U = TopOpen K
3 2 simp2d U UnifOn X U = UnifSet K