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)

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 df-tset ⊢ TopSet = Slot 9
3 1lt9 ⊢ 1 < 9
4 9nn ⊢ 9 ∈ ℕ
5 1 2 3 4 2strop ⊢ J ∈ TopOn ⁡ A → J = TopSet ⁡ K
6 toponmax ⊢ J ∈ TopOn ⁡ A → A ∈ J
7 1 2 3 4 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