Theorem onintopssconn

Description: An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015)

	Ref	Expression
Assertion	onintopssconn	⊢ ( On ∩ Top ) ⊆ Conn

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑥 ∈ ( On ∩ Top ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ Top ) )
2		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
3		ordtopconn	⊢ ( Ord 𝑥 → ( 𝑥 ∈ Top ↔ 𝑥 ∈ Conn ) )
4	2 3	syl	⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ Top ↔ 𝑥 ∈ Conn ) )
5	4	biimpa	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ Top ) → 𝑥 ∈ Conn )
6	1 5	sylbi	⊢ ( 𝑥 ∈ ( On ∩ Top ) → 𝑥 ∈ Conn )
7	6	ssriv	⊢ ( On ∩ Top ) ⊆ Conn