Theorem indistps2ALT

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

	Ref	Expression
Hypotheses	indistps2ALT.a	|- ( Base ` K ) = A
	indistps2ALT.j	|- ( TopOpen ` K ) = { (/) , A }
Assertion	indistps2ALT	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		indistps2ALT.a	|- ( Base ` K ) = A
2		indistps2ALT.j	|- ( TopOpen ` K ) = { (/) , A }
3		fvex	|- ( Base ` K ) e. _V
4	1 3	eqeltrri	|- A e. _V
5		indistopon	|- ( A e. _V -> { (/) , A } e. ( TopOn ` A ) )
6	4 5	ax-mp	|- { (/) , A } e. ( TopOn ` A )
7	1	eqcomi	|- A = ( Base ` K )
8	2	eqcomi	|- { (/) , A } = ( TopOpen ` K )
9	7 8	istps	|- ( K e. TopSp <-> { (/) , A } e. ( TopOn ` A ) )
10	6 9	mpbir	|- K e. TopSp