Metamath Proof Explorer

Theorem tustps

Description: A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018)

Ref Expression
Hypothesis tuslem.k ⊢ K = toUnifSp ⁡ U
Assertion tustps ⊢ U ∈ UnifOn ⁡ X → K ∈ TopSp

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ K = toUnifSp ⁡ U
2 utoptopon ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U ∈ TopOn ⁡ X
3 eqid ⊢ unifTop ⁡ U = unifTop ⁡ U
4 1 3 tustopn ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopOpen ⁡ K
5 1 tusbas ⊢ U ∈ UnifOn ⁡ X → X = Base K
6 5 fveq2d ⊢ U ∈ UnifOn ⁡ X → TopOn ⁡ X = TopOn ⁡ Base K
7 2 4 6 3eltr3d ⊢ U ∈ UnifOn ⁡ X → TopOpen ⁡ K ∈ TopOn ⁡ Base K
8 eqid ⊢ Base K = Base K
9 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
10 8 9 istps ⊢ K ∈ TopSp ↔ TopOpen ⁡ K ∈ TopOn ⁡ Base K
11 7 10 sylibr ⊢ U ∈ UnifOn ⁡ X → K ∈ TopSp