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

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 ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
Assertion tustps ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
2 utoptopon ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) )
3 eqid ⊢ ( unifTop ‘ 𝑈 ) = ( unifTop ‘ 𝑈 )
4 1 3 tustopn ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) )
5 1 tusbas ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
6 5 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
7 2 4 6 3eltr3d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
10 8 9 istps ⊢ ( 𝐾 ∈ TopSp ↔ ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
11 7 10 sylibr ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 ∈ TopSp )