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

Metamath Proof Explorer

Theorem tsettps

Description: If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses tsettps.a ⊢ A = Base K
tsettps.j ⊢ J = TopSet ⁡ K
Assertion tsettps ⊢ J ∈ TopOn ⁡ A → K ∈ TopSp

Proof

Step Hyp Ref Expression
1 tsettps.a ⊢ A = Base K
2 tsettps.j ⊢ J = TopSet ⁡ K
3 1 2 topontopn ⊢ J ∈ TopOn ⁡ A → J = TopOpen ⁡ K
4 id ⊢ J ∈ TopOn ⁡ A → J ∈ TopOn ⁡ A
5 3 4 eqeltrrd ⊢ J ∈ TopOn ⁡ A → TopOpen ⁡ K ∈ TopOn ⁡ A
6 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
7 1 6 istps ⊢ K ∈ TopSp ↔ TopOpen ⁡ K ∈ TopOn ⁡ A
8 5 7 sylibr ⊢ J ∈ TopOn ⁡ A → K ∈ TopSp