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