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	|- A e. _V
	indistpsALT.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. }
Assertion	indistpsALT	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		indistpsALT.a	|- A e. _V
2		indistpsALT.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. }
3		indistopon	|- ( A e. _V -> { (/) , A } e. ( TopOn ` A ) )
4		basendxlttsetndx	|- ( Base ` ndx ) < ( TopSet ` ndx )
5		tsetndxnn	|- ( TopSet ` ndx ) e. NN
6	2 4 5	2strbas	|- ( A e. _V -> A = ( Base ` K ) )
7	1 6	ax-mp	|- A = ( Base ` K )
8		prex	|- { (/) , A } e. _V
9		tsetid	|- TopSet = Slot ( TopSet ` ndx )
10	2 4 5 9	2strop	|- ( { (/) , A } e. _V -> { (/) , A } = ( TopSet ` K ) )
11	8 10	ax-mp	|- { (/) , A } = ( TopSet ` K )
12	7 11	tsettps	|- ( { (/) , A } e. ( TopOn ` A ) -> K e. TopSp )
13	1 3 12	mp2b	|- K e. TopSp