Theorem onintopssconn

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

	Ref	Expression
Assertion	onintopssconn	|- ( On i^i Top ) C_ Conn

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( x e. ( On i^i Top ) <-> ( x e. On /\ x e. Top ) )
2		eloni	|- ( x e. On -> Ord x )
3		ordtopconn	|- ( Ord x -> ( x e. Top <-> x e. Conn ) )
4	2 3	syl	|- ( x e. On -> ( x e. Top <-> x e. Conn ) )
5	4	biimpa	|- ( ( x e. On /\ x e. Top ) -> x e. Conn )
6	1 5	sylbi	|- ( x e. ( On i^i Top ) -> x e. Conn )
7	6	ssriv	|- ( On i^i Top ) C_ Conn