Theorem ordttop

Description: The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	ordttop	⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ dom 𝑅 = dom 𝑅
2	1	ordttopon	⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
3		topontop	⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) → ( ordTop ‘ 𝑅 ) ∈ Top )
4	2 3	syl	⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) ∈ Top )