Metamath Proof Explorer


Theorem utoptopon

Description: Topology induced by a uniform structure U with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018)

Ref Expression
Assertion utoptopon U UnifOn X unifTop U TopOn X

Proof

Step Hyp Ref Expression
1 utoptop U UnifOn X unifTop U Top
2 utopbas U UnifOn X X = unifTop U
3 istopon unifTop U TopOn X unifTop U Top X = unifTop U
4 1 2 3 sylanbrc U UnifOn X unifTop U TopOn X