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 )