Theorem distps

Description: The discrete topology on a set A expressed as a topological space. (Contributed by FL, 20-Aug-2006)

	Ref	Expression
Hypotheses	distps.a	$$⊢A\in \mathrm{V}$$
	distps.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),𝒫A⟩\right\}$$
Assertion	distps	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		distps.a	$$⊢A\in \mathrm{V}$$
2		distps.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},A⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),𝒫A⟩\right\}$$
3		unipw	$$⊢\bigcup 𝒫A=A$$
4	3	eqcomi	$$⊢A=\bigcup 𝒫A$$
5		distop	$$⊢A\in \mathrm{V}\to 𝒫A\in \mathrm{Top}$$
6	1 5	ax-mp	$$⊢𝒫A\in \mathrm{Top}$$
7	2 4 6	eltpsi	$$⊢K\in \mathrm{TopSp}$$