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\in \mathrm{V}$$
	indistpsALT.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\left\{\varnothing ,A\right\}⟩\right\}$$
Assertion	indistpsALT	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		indistpsALT.a	$$⊢A\in \mathrm{V}$$
2		indistpsALT.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\left\{\varnothing ,A\right\}⟩\right\}$$
3		indistopon	$$⊢A\in \mathrm{V}\to \left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
4		df-tset	$$⊢\mathrm{TopSet}=\mathrm{Slot}9$$
5		1lt9	$$⊢1<9$$
6		9nn	$$⊢9\in \mathbb{N}$$
7	2 4 5 6	2strbas	$$⊢A\in \mathrm{V}\to A={\mathrm{Base}}_K$$
8	1 7	ax-mp	$$⊢A={\mathrm{Base}}_K$$
9		prex	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{V}$$
10	2 4 5 6	2strop	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{V}\to \left\{\varnothing ,A\right\}=\mathrm{TopSet}\left(K\right)$$
11	9 10	ax-mp	$$⊢\left\{\varnothing ,A\right\}=\mathrm{TopSet}\left(K\right)$$
12	8 11	tsettps	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)\to K\in \mathrm{TopSp}$$
13	1 3 12	mp2b	$$⊢K\in \mathrm{TopSp}$$