Theorem distopon

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

	Ref	Expression
Assertion	distopon	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		distop	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
3	2	eqcomi	⊢ 𝐴 = ∪ 𝒫 𝐴
4		istopon	⊢ ( 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) ↔ ( 𝒫 𝐴 ∈ Top ∧ 𝐴 = ∪ 𝒫 𝐴 ) )
5	1 3 4	sylanblrc	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) )