Metamath Proof Explorer

Theorem ordttop

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

Ref Expression
Assertion ordttop 
|- ( R e. V -> ( ordTop ` R ) e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom R = dom R
2 1 ordttopon 
 |-  ( R e. V -> ( ordTop ` R ) e. ( TopOn ` dom R ) )
3 topontop 
 |-  ( ( ordTop ` R ) e. ( TopOn ` dom R ) -> ( ordTop ` R ) e. Top )
4 2 3 syl 
 |-  ( R e. V -> ( ordTop ` R ) e. Top )