Theorem ordtopt0

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

	Ref	Expression
Assertion	ordtopt0	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\leftrightarrow J\in \mathrm{Kol2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtop	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\leftrightarrow J\ne \bigcup J\right)$$
2		onsuct0	$$⊢\bigcup J\in \mathrm{On}\to \mathrm{suc}\bigcup J\in \mathrm{Kol2}$$
3	2	ordtoplem	$$⊢\mathrm{Ord}J\to \left(J\ne \bigcup J\to J\in \mathrm{Kol2}\right)$$
4	1 3	sylbid	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\to J\in \mathrm{Kol2}\right)$$
5		t0top	$$⊢J\in \mathrm{Kol2}\to J\in \mathrm{Top}$$
6	4 5	impbid1	$$⊢\mathrm{Ord}J\to \left(J\in \mathrm{Top}\leftrightarrow J\in \mathrm{Kol2}\right)$$