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) (Revised by AV, 31-Oct-2024) (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		basendxlttsetndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
5		tsetndxnn	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathbb{N}$$
6	2 4 5	2strbas1	$$⊢A\in \mathrm{V}\to A={\mathrm{Base}}_K$$
7	1 6	ax-mp	$$⊢A={\mathrm{Base}}_K$$
8		prex	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{V}$$
9		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
10	2 4 5 9	2strop1	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{V}\to \left\{\varnothing ,A\right\}=\mathrm{TopSet}\left(K\right)$$
11	8 10	ax-mp	$$⊢\left\{\varnothing ,A\right\}=\mathrm{TopSet}\left(K\right)$$
12	7 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}$$