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 e. _V
	distps.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ~P A >. }
Assertion	distps	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		distps.a	|- A e. _V
2		distps.k	|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ~P A >. }
3		unipw	|- U. ~P A = A
4	3	eqcomi	|- A = U. ~P A
5		distop	|- ( A e. _V -> ~P A e. Top )
6	1 5	ax-mp	|- ~P A e. Top
7	2 4 6	eltpsi	|- K e. TopSp