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={\mathrm{Base}}_K$$
	ordtconn.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
	ordtconn.j	$$⊢J=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
Assertion	ordtconn	$$⊢\top$$

Proof

Step	Hyp	Ref	Expression
1		ordtconn.x	$$⊢B={\mathrm{Base}}_K$$
2		ordtconn.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
3		ordtconn.j	$$⊢J=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
4		tru	$$⊢\top$$