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 ∈ Top ↔ J ∈ Kol2

Proof

Step Hyp Ref Expression
1 ordtop ⊢ Ord ⁡ J → J ∈ Top ↔ J ≠ ⋃ J
2 onsuct0 ⊢ ⋃ J ∈ On → suc ⁡ ⋃ J ∈ Kol2
3 2 ordtoplem ⊢ Ord ⁡ J → J ≠ ⋃ J → J ∈ Kol2
4 1 3 sylbid ⊢ Ord ⁡ J → J ∈ Top → J ∈ Kol2
5 t0top ⊢ J ∈ Kol2 → J ∈ Top
6 4 5 impbid1 ⊢ Ord ⁡ J → J ∈ Top ↔ J ∈ Kol2