Theorem distopon

Description: The discrete topology on a set A , with base set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	distopon	$$⊢A\in V\to 𝒫A\in \mathrm{TopOn}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		distop	$$⊢A\in V\to 𝒫A\in \mathrm{Top}$$
2		unipw	$$⊢\bigcup 𝒫A=A$$
3	2	eqcomi	$$⊢A=\bigcup 𝒫A$$
4		istopon	$$⊢𝒫A\in \mathrm{TopOn}\left(A\right)\leftrightarrow \left(𝒫A\in \mathrm{Top}\wedge A=\bigcup 𝒫A\right)$$
5	1 3 4	sylanblrc	$$⊢A\in V\to 𝒫A\in \mathrm{TopOn}\left(A\right)$$