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 | ⊢ 𝐴 = ( Base ‘ 𝐾 ) | |
tsettps.j | ⊢ 𝐽 = ( TopSet ‘ 𝐾 ) | ||
Assertion | tsettps | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsettps.a | ⊢ 𝐴 = ( Base ‘ 𝐾 ) | |
2 | tsettps.j | ⊢ 𝐽 = ( TopSet ‘ 𝐾 ) | |
3 | 1 2 | topontopn | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 = ( TopOpen ‘ 𝐾 ) ) |
4 | id | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) | |
5 | 3 4 | eqeltrrd | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ 𝐴 ) ) |
6 | eqid | ⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) | |
7 | 1 6 | istps | ⊢ ( 𝐾 ∈ TopSp ↔ ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ 𝐴 ) ) |
8 | 5 7 | sylibr | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp ) |