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 \in V \land S \in W \land F {Isom}_{R, S} (X, Y)) \to F \in (ordTop (R) Homeo ordTop (S))$

Step	Hyp	Ref	Expression
1		ordthmeo.1	$⊢ X = dom R$
2		ordthmeo.2	$⊢ Y = dom S$
3	1 2	ordthmeolem	$⊢ (R \in V \land S \in W \land F {Isom}_{R, S} (X, Y)) \to F \in (ordTop (R) Cn ordTop (S))$
4		isocnv	$⊢ F {Isom}_{R, S} (X, Y) \to F^{-1} {Isom}_{S, R} (Y, X)$
5	2 1	ordthmeolem	$⊢ (S \in W \land R \in V \land F^{-1} {Isom}_{S, R} (Y, X)) \to F^{-1} \in (ordTop (S) Cn ordTop (R))$
6	5	3com12	$⊢ (R \in V \land S \in W \land F^{-1} {Isom}_{S, R} (Y, X)) \to F^{-1} \in (ordTop (S) Cn ordTop (R))$
7	4 6	syl3an3	$⊢ (R \in V \land S \in W \land F {Isom}_{R, S} (X, Y)) \to F^{-1} \in (ordTop (S) Cn ordTop (R))$
8		ishmeo	$⊢ F \in (ordTop (R) Homeo ordTop (S)) \leftrightarrow (F \in (ordTop (R) Cn ordTop (S)) \land F^{-1} \in (ordTop (S) Cn ordTop (R)))$
9	3 7 8	sylanbrc	$⊢ (R \in V \land S \in W \land F {Isom}_{R, S} (X, Y)) \to F \in (ordTop (R) Homeo ordTop (S))$

Metamath Proof Explorer