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	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		utoptop	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )
2		utopbas	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )
3		istopon	⊢ ( ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) ↔ ( ( unifTop ‘ 𝑈 ) ∈ Top ∧ 𝑋 = ∪ ( unifTop ‘ 𝑈 ) ) )
4	1 2 3	sylanbrc	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ ( TopOn ‘ 𝑋 ) )