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}\left(A,B\right)\to \left(R\mathrm{Or}A\leftrightarrow S\mathrm{Or}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		isocnv	$$⊢H{Isom}_{R,S}\left(A,B\right)\to H^{-1}{Isom}_{S,R}\left(B,A\right)$$
2		isosolem	$$⊢H^{-1}{Isom}_{S,R}\left(B,A\right)\to \left(R\mathrm{Or}A\to S\mathrm{Or}B\right)$$
3	1 2	syl	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{Or}A\to S\mathrm{Or}B\right)$$
4		isosolem	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(S\mathrm{Or}B\to R\mathrm{Or}A\right)$$
5	3 4	impbid	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{Or}A\leftrightarrow S\mathrm{Or}B\right)$$