This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoso

Description: An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion isoso ⊢ H Isom R , S A B → R Or A ↔ S Or B

Proof

Step Hyp Ref Expression
1 isocnv ⊢ H Isom R , S A B → H -1 Isom S , R B A
2 isosolem ⊢ H -1 Isom S , R B A → R Or A → S Or B
3 1 2 syl ⊢ H Isom R , S A B → R Or A → S Or B
4 isosolem ⊢ H Isom R , S A B → S Or B → R Or A
5 3 4 impbid ⊢ H Isom R , S A B → R Or A ↔ S Or B