Theorem indistpsx

Description: The indiscrete topology on a set A expressed as a topological space, using explicit structure component references. Compare with indistps and indistps2 . The advantage of this version is that the actual function for the structure is evident, and df-ndx is not needed, nor any other special definition outside of basic set theory. The disadvantage is that if the indices of the component definitions df-base and df-tset are changed in the future, this theorem will also have to be changed. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use indistps instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006)

	Ref	Expression
Hypotheses	indistpsx.a	|- A e. _V
	indistpsx.k	|- K = { <. 1 , A >. , <. 9 , { (/) , A } >. }
Assertion	indistpsx	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		indistpsx.a	|- A e. _V
2		indistpsx.k	|- K = { <. 1 , A >. , <. 9 , { (/) , A } >. }
3		basendx	|- ( Base ` ndx ) = 1
4	3	opeq1i	|- <. ( Base ` ndx ) , A >. = <. 1 , A >.
5		tsetndx	|- ( TopSet ` ndx ) = 9
6	5	opeq1i	|- <. ( TopSet ` ndx ) , { (/) , A } >. = <. 9 , { (/) , A } >.
7	4 6	preq12i	|- { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. } = { <. 1 , A >. , <. 9 , { (/) , A } >. }
8	2 7	eqtr4i	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. }
9		indistopon	|- ( A e. _V -> { (/) , A } e. ( TopOn ` A ) )
10	1 9	ax-mp	|- { (/) , A } e. ( TopOn ` A )
11	10	toponunii	|- A = U. { (/) , A }
12		indistop	|- { (/) , A } e. Top
13	8 11 12	eltpsi	|- K e. TopSp