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	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion	dissneq	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ ( TopOn ‘ 𝐴 ) ) → 𝐵 = 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dissneq.c	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
2		sneq	⊢ ( 𝑧 = 𝑥 → { 𝑧 } = { 𝑥 } )
3	2	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑢 = { 𝑧 } ↔ 𝑢 = { 𝑥 } ) )
4	3	cbvrexvw	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑢 = { 𝑧 } ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } )
5	4	abbii	⊢ { 𝑢 ∣ ∃ 𝑧 ∈ 𝐴 𝑢 = { 𝑧 } } = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
6	1 5	eqtr4i	⊢ 𝐶 = { 𝑢 ∣ ∃ 𝑧 ∈ 𝐴 𝑢 = { 𝑧 } }
7	6	dissneqlem	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ ( TopOn ‘ 𝐴 ) ) → 𝐵 = 𝒫 𝐴 )