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

Proof

Step Hyp Ref Expression
1 eltpsi.k 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
2 df-tset TopSet = Slot 9
3 1lt9 1 < 9
4 9nn 9 ∈ ℕ
5 1 2 3 4 2strop ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 = ( TopSet ‘ 𝐾 ) )
6 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐴𝐽 )
7 1 2 3 4 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 )