This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordthmeo

Description: An order isomorphism is a homeomorphism on the respective order topologies. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordthmeo.1 
|- X = dom R
ordthmeo.2 
|- Y = dom S
Assertion ordthmeo 
|- ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Homeo ( ordTop ` S ) ) )

Proof

Step Hyp Ref Expression
1 ordthmeo.1 
 |-  X = dom R
2 ordthmeo.2 
 |-  Y = dom S
3 1 2 ordthmeolem 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Cn ( ordTop ` S ) ) )
4 isocnv 
 |-  ( F Isom R , S ( X , Y ) -> `' F Isom S , R ( Y , X ) )
5 2 1 ordthmeolem 
 |-  ( ( S e. W /\ R e. V /\ `' F Isom S , R ( Y , X ) ) -> `' F e. ( ( ordTop ` S ) Cn ( ordTop ` R ) ) )
6 5 3com12 
 |-  ( ( R e. V /\ S e. W /\ `' F Isom S , R ( Y , X ) ) -> `' F e. ( ( ordTop ` S ) Cn ( ordTop ` R ) ) )
7 4 6 syl3an3 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> `' F e. ( ( ordTop ` S ) Cn ( ordTop ` R ) ) )
8 ishmeo 
 |-  ( F e. ( ( ordTop ` R ) Homeo ( ordTop ` S ) ) <-> ( F e. ( ( ordTop ` R ) Cn ( ordTop ` S ) ) /\ `' F e. ( ( ordTop ` S ) Cn ( ordTop ` R ) ) ) )
9 3 7 8 sylanbrc 
 |-  ( ( R e. V /\ S e. W /\ F Isom R , S ( X , Y ) ) -> F e. ( ( ordTop ` R ) Homeo ( ordTop ` S ) ) )