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 )