Theorem dissneq

Description: Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020)

	Ref	Expression
Hypothesis	dissneq.c	$$⊢C=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
Assertion	dissneq	$$⊢\left(C\subseteq B\wedge B\in \mathrm{TopOn}\left(A\right)\right)\to B=𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		dissneq.c	$$⊢C=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
2		sneq	$$⊢z=x\to \left\{z\right\}=\left\{x\right\}$$
3	2	eqeq2d	$$⊢z=x\to \left(u=\left\{z\right\}\leftrightarrow u=\left\{x\right\}\right)$$
4	3	cbvrexvw	$$⊢\exists z\in Au=\left\{z\right\}\leftrightarrow \exists x\in Au=\left\{x\right\}$$
5	4	abbii	$$⊢\left\{u|\exists z\in Au=\left\{z\right\}\right\}=\left\{u|\exists x\in Au=\left\{x\right\}\right\}$$
6	1 5	eqtr4i	$$⊢C=\left\{u|\exists z\in Au=\left\{z\right\}\right\}$$
7	6	dissneqlem	$$⊢\left(C\subseteq B\wedge B\in \mathrm{TopOn}\left(A\right)\right)\to B=𝒫A$$