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	$$⊢{\mathrm{Base}}_K=A$$
	indistps2ALT.j	$$⊢\mathrm{TopOpen}\left(K\right)=\left\{\varnothing ,A\right\}$$
Assertion	indistps2ALT	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		indistps2ALT.a	$$⊢{\mathrm{Base}}_K=A$$
2		indistps2ALT.j	$$⊢\mathrm{TopOpen}\left(K\right)=\left\{\varnothing ,A\right\}$$
3		fvex	$$⊢{\mathrm{Base}}_K\in \mathrm{V}$$
4	1 3	eqeltrri	$$⊢A\in \mathrm{V}$$
5		indistopon	$$⊢A\in \mathrm{V}\to \left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
6	4 5	ax-mp	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
7	1	eqcomi	$$⊢A={\mathrm{Base}}_K$$
8	2	eqcomi	$$⊢\left\{\varnothing ,A\right\}=\mathrm{TopOpen}\left(K\right)$$
9	7 8	istps	$$⊢K\in \mathrm{TopSp}\leftrightarrow \left\{\varnothing ,A\right\}\in \mathrm{TopOn}\left(A\right)$$
10	6 9	mpbir	$$⊢K\in \mathrm{TopSp}$$