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\in \mathrm{V}$$
	indistpsx.k	$$⊢K=\left\{⟨1,A⟩,⟨9,\left\{\varnothing ,A\right\}⟩\right\}$$
Assertion	indistpsx	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		indistpsx.a	$$⊢A\in \mathrm{V}$$
2		indistpsx.k	$$⊢K=\left\{⟨1,A⟩,⟨9,\left\{\varnothing ,A\right\}⟩\right\}$$
3		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4	3	opeq1i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩=⟨1,A⟩$$
5		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
6	5	opeq1i	$$⊢⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\left\{\varnothing ,A\right\}⟩=⟨9,\left\{\varnothing ,A\right\}⟩$$
7	4 6	preq12i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\left\{\varnothing ,A\right\}⟩\right\}=\left\{⟨1,A⟩,⟨9,\left\{\varnothing ,A\right\}⟩\right\}$$
8	2 7	eqtr4i	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\left\{\varnothing ,A\right\}⟩\right\}$$
9		indistopon	$$⊢A\in \mathrm{V}\to \left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
10	1 9	ax-mp	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
11	10	toponunii	$$⊢A=\bigcup \left\{\varnothing ,A\right\}$$
12		indistop	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}$$
13	8 11 12	eltpsi	$$⊢K\in \mathrm{TopSp}$$