Theorem indistpsALT

Description: The indiscrete topology on a set A expressed as a topological space. Here we show how to derive the structural version indistps from the direct component assignment version indistps2 . (Contributed by NM, 24-Oct-2012) (Revised by AV, 31-Oct-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	indistpsALT.a	⊢ 𝐴 ∈ V
	indistpsALT.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
Assertion	indistpsALT	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		indistpsALT.a	⊢ 𝐴 ∈ V
2		indistpsALT.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
3		indistopon	⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
4		basendxlttsetndx	⊢ ( Base ‘ ndx ) < ( TopSet ‘ ndx )
5		tsetndxnn	⊢ ( TopSet ‘ ndx ) ∈ ℕ
6	2 4 5	2strbas	⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ 𝐾 ) )
7	1 6	ax-mp	⊢ 𝐴 = ( Base ‘ 𝐾 )
8		prex	⊢ { ∅ , 𝐴 } ∈ V
9		tsetid	⊢ TopSet = Slot ( TopSet ‘ ndx )
10	2 4 5 9	2strop	⊢ ( { ∅ , 𝐴 } ∈ V → { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) )
11	8 10	ax-mp	⊢ { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 )
12	7 11	tsettps	⊢ ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )
13	1 3 12	mp2b	⊢ 𝐾 ∈ TopSp