Theorem ordtopconn

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

	Ref	Expression
Assertion	ordtopconn	⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ∈ Conn ) )

Proof

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