Metamath Proof Explorer

Theorem ordttop

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

Ref Expression
Assertion ordttop ⊢ R ∈ V → ordTop ⁡ R ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom ⁡ R = dom ⁡ R
2 1 ordttopon ⊢ R ∈ V → ordTop ⁡ R ∈ TopOn ⁡ dom ⁡ R
3 topontop ⊢ ordTop ⁡ R ∈ TopOn ⁡ dom ⁡ R → ordTop ⁡ R ∈ Top
4 2 3 syl ⊢ R ∈ V → ordTop ⁡ R ∈ Top