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 ⊢ 𝑋 = dom 𝑅
ordthmeo.2 ⊢ 𝑌 = dom 𝑆
Assertion ordthmeo ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Homeo ( ordTop ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ordthmeo.1 ⊢ 𝑋 = dom 𝑅
2 ordthmeo.2 ⊢ 𝑌 = dom 𝑆
3 1 2 ordthmeolem ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Cn ( ordTop ‘ 𝑆 ) ) )
4 isocnv ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) → ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝑌 , 𝑋 ) )
5 2 1 ordthmeolem ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑅 ∈ 𝑉 ∧ ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝑌 , 𝑋 ) ) → ◡ 𝐹 ∈ ( ( ordTop ‘ 𝑆 ) Cn ( ordTop ‘ 𝑅 ) ) )
6 5 3com12 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ ◡ 𝐹 Isom 𝑆 , 𝑅 ( 𝑌 , 𝑋 ) ) → ◡ 𝐹 ∈ ( ( ordTop ‘ 𝑆 ) Cn ( ordTop ‘ 𝑅 ) ) )
7 4 6 syl3an3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → ◡ 𝐹 ∈ ( ( ordTop ‘ 𝑆 ) Cn ( ordTop ‘ 𝑅 ) ) )
8 ishmeo ⊢ ( 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Homeo ( ordTop ‘ 𝑆 ) ) ↔ ( 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Cn ( ordTop ‘ 𝑆 ) ) ∧ ◡ 𝐹 ∈ ( ( ordTop ‘ 𝑆 ) Cn ( ordTop ‘ 𝑅 ) ) ) )
9 3 7 8 sylanbrc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅 , 𝑆 ( 𝑋 , 𝑌 ) ) → 𝐹 ∈ ( ( ordTop ‘ 𝑅 ) Homeo ( ordTop ‘ 𝑆 ) ) )