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 ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
Assertion eltpsg ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 eltpsi.k ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
2 basendxlttsetndx ⊢ ( Base ‘ ndx ) < ( TopSet ‘ ndx )
3 tsetndxnn ⊢ ( TopSet ‘ ndx ) ∈ ℕ
4 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
5 1 2 3 4 2strop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 = ( TopSet ‘ 𝐾 ) )
6 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ 𝐽 )
7 1 2 3 2strbas ⊢ ( 𝐴 ∈ 𝐽 → 𝐴 = ( Base ‘ 𝐾 ) )
8 6 7 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐴 = ( Base ‘ 𝐾 ) )
9 8 fveq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( TopOn ‘ 𝐴 ) = ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
10 5 9 eleq12d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ↔ ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ) )
11 10 ibi ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 eqid ⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
14 12 13 tsettps ⊢ ( ( TopSet ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ TopSp )
15 11 14 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )