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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ordtconn.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
	ordtconn.j	⊢ 𝐽 = ( ordTop ‘ ≤ )
Assertion	ordtconn	⊢ ⊤

Proof

Step	Hyp	Ref	Expression
1		ordtconn.x	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ordtconn.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3		ordtconn.j	⊢ 𝐽 = ( ordTop ‘ ≤ )
4		tru	⊢ ⊤