This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem distps

Description: The discrete topology on a set A expressed as a topological space. (Contributed by FL, 20-Aug-2006)

Ref Expression
Hypotheses distps.a ⊢ A ∈ V
distps.k ⊢ K = Base ndx A TopSet ⁡ ndx 𝒫 A
Assertion distps ⊢ K ∈ TopSp

Proof

Step Hyp Ref Expression
1 distps.a ⊢ A ∈ V
2 distps.k ⊢ K = Base ndx A TopSet ⁡ ndx 𝒫 A
3 unipw ⊢ ⋃ 𝒫 A = A
4 3 eqcomi ⊢ A = ⋃ 𝒫 A
5 distop ⊢ A ∈ V → 𝒫 A ∈ Top
6 1 5 ax-mp ⊢ 𝒫 A ∈ Top
7 2 4 6 eltpsi ⊢ K ∈ TopSp