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 = { u | E. x e. A u = { x } }
Assertion	dissneq	|- ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B = ~P A )

Proof

Step	Hyp	Ref	Expression
1		dissneq.c	|- C = { u | E. x e. A u = { x } }
2		sneq	|- ( z = x -> { z } = { x } )
3	2	eqeq2d	|- ( z = x -> ( u = { z } <-> u = { x } ) )
4	3	cbvrexvw	|- ( E. z e. A u = { z } <-> E. x e. A u = { x } )
5	4	abbii	|- { u | E. z e. A u = { z } } = { u | E. x e. A u = { x } }
6	1 5	eqtr4i	|- C = { u | E. z e. A u = { z } }
7	6	dissneqlem	|- ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B = ~P A )