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