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