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 ∈ V ∧ S ∈ W ∧ F Isom R , S X Y → F ∈ 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 ∈ V ∧ S ∈ W ∧ F Isom R , S X Y → F ∈ ordTop ⁡ R Cn ordTop ⁡ S
4 isocnv ⊢ F Isom R , S X Y → F -1 Isom S , R Y X
5 2 1 ordthmeolem ⊢ S ∈ W ∧ R ∈ V ∧ F -1 Isom S , R Y X → F -1 ∈ ordTop ⁡ S Cn ordTop ⁡ R
6 5 3com12 ⊢ R ∈ V ∧ S ∈ W ∧ F -1 Isom S , R Y X → F -1 ∈ ordTop ⁡ S Cn ordTop ⁡ R
7 4 6 syl3an3 ⊢ R ∈ V ∧ S ∈ W ∧ F Isom R , S X Y → F -1 ∈ ordTop ⁡ S Cn ordTop ⁡ R
8 ishmeo ⊢ F ∈ ordTop ⁡ R Homeo ordTop ⁡ S ↔ F ∈ ordTop ⁡ R Cn ordTop ⁡ S ∧ F -1 ∈ ordTop ⁡ S Cn ordTop ⁡ R
9 3 7 8 sylanbrc ⊢ R ∈ V ∧ S ∈ W ∧ F Isom R , S X Y → F ∈ ordTop ⁡ R Homeo ordTop ⁡ S