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 Isom S , R ( B , A ) )
2		isosolem	|- ( `' H 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 ) )