Metamath Proof Explorer

Theorem ordtopt0

Description: An ordinal topology is T_0. (Contributed by Chen-Pang He, 8-Nov-2015)

Ref Expression
Assertion ordtopt0 
|- ( Ord J -> ( J e. Top <-> J e. Kol2 ) )

Proof

Step Hyp Ref Expression
1 ordtop 
 |-  ( Ord J -> ( J e. Top <-> J =/= U. J ) )
2 onsuct0 
 |-  ( U. J e. On -> suc U. J e. Kol2 )
3 2 ordtoplem 
 |-  ( Ord J -> ( J =/= U. J -> J e. Kol2 ) )
4 1 3 sylbid 
 |-  ( Ord J -> ( J e. Top -> J e. Kol2 ) )
5 t0top 
 |-  ( J e. Kol2 -> J e. Top )
6 4 5 impbid1 
 |-  ( Ord J -> ( J e. Top <-> J e. Kol2 ) )