Theorem eltpsi

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

	Ref	Expression
Hypotheses	eltpsi.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
	eltpsi.u	⊢ 𝐴 = ∪ 𝐽
	eltpsi.j	⊢ 𝐽 ∈ Top
Assertion	eltpsi	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		eltpsi.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ }
2		eltpsi.u	⊢ 𝐴 = ∪ 𝐽
3		eltpsi.j	⊢ 𝐽 ∈ Top
4	2	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
5	3 4	mpbi	⊢ 𝐽 ∈ ( TopOn ‘ 𝐴 )
6	1	eltpsg	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )
7	5 6	ax-mp	⊢ 𝐾 ∈ TopSp