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