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 ) ) )`