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) (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		df-tset	|- TopSet = Slot 9
5		1lt9	|- 1 < 9
6		9nn	|- 9 e. NN
7	2 4 5 6	2strbas	|- ( A e. _V -> A = ( Base ` K ) )
8	1 7	ax-mp	|- A = ( Base ` K )
9		prex	|- { (/) , A } e. _V
10	2 4 5 6	2strop	|- ( { (/) , A } e. _V -> { (/) , A } = ( TopSet ` K ) )
11	9 10	ax-mp	|- { (/) , A } = ( TopSet ` K )
12	8 11	tsettps	|- ( { (/) , A } e. ( TopOn ` A ) -> K e. TopSp )
13	1 3 12	mp2b	|- K e. TopSp