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 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