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

Metamath Proof Explorer

Theorem eltpsg

Description: Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypothesis eltpsi.k ⊢ K = Base ndx A TopSet ⁡ ndx J
Assertion eltpsg ⊢ J ∈ TopOn ⁡ A → K ∈ TopSp

Proof

Step Hyp Ref Expression
1 eltpsi.k ⊢ K = Base ndx A TopSet ⁡ ndx J
2 basendxlttsetndx ⊢ Base ndx < TopSet ⁡ ndx
3 tsetndxnn ⊢ TopSet ⁡ ndx ∈ ℕ
4 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
5 1 2 3 4 2strop ⊢ J ∈ TopOn ⁡ A → J = TopSet ⁡ K
6 toponmax ⊢ J ∈ TopOn ⁡ A → A ∈ J
7 1 2 3 2strbas ⊢ A ∈ J → A = Base K
8 6 7 syl ⊢ J ∈ TopOn ⁡ A → A = Base K
9 8 fveq2d ⊢ J ∈ TopOn ⁡ A → TopOn ⁡ A = TopOn ⁡ Base K
10 5 9 eleq12d ⊢ J ∈ TopOn ⁡ A → J ∈ TopOn ⁡ A ↔ TopSet ⁡ K ∈ TopOn ⁡ Base K
11 10 ibi ⊢ J ∈ TopOn ⁡ A → TopSet ⁡ K ∈ TopOn ⁡ Base K
12 eqid ⊢ Base K = Base K
13 eqid ⊢ TopSet ⁡ K = TopSet ⁡ K
14 12 13 tsettps ⊢ TopSet ⁡ K ∈ TopOn ⁡ Base K → K ∈ TopSp
15 11 14 syl ⊢ J ∈ TopOn ⁡ A → K ∈ TopSp