Theorem ordtopconn

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

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

Proof

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