Theorem ordtopt0

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

	Ref	Expression
Assertion	ordtopt0	⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ∈ Kol2 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtop	⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽 ) )
2		onsuct0	⊢ ( ∪ 𝐽 ∈ On → suc ∪ 𝐽 ∈ Kol2 )
3	2	ordtoplem	⊢ ( Ord 𝐽 → ( 𝐽 ≠ ∪ 𝐽 → 𝐽 ∈ Kol2 ) )
4	1 3	sylbid	⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top → 𝐽 ∈ Kol2 ) )
5		t0top	⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
6	4 5	impbid1	⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ∈ Kol2 ) )