Theorem ordtconn

Description: Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018)

	Ref	Expression
Hypotheses	ordtconn.x	|- B = ( Base ` K )
	ordtconn.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
	ordtconn.j	|- J = ( ordTop ` .<_ )
Assertion	ordtconn	|- T.

Proof

Step	Hyp	Ref	Expression
1		ordtconn.x	|- B = ( Base ` K )
2		ordtconn.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
3		ordtconn.j	|- J = ( ordTop ` .<_ )
4		tru	|- T.