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	⊢ 𝐴 ∈ V
	distps.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝒫 𝐴 ⟩ }
Assertion	distps	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		distps.a	⊢ 𝐴 ∈ V
2		distps.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝒫 𝐴 ⟩ }
3		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
4	3	eqcomi	⊢ 𝐴 = ∪ 𝒫 𝐴
5		distop	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ Top )
6	1 5	ax-mp	⊢ 𝒫 𝐴 ∈ Top
7	2 4 6	eltpsi	⊢ 𝐾 ∈ TopSp