Theorem isopo

Description: An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Assertion	isopo	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{Po}A\leftrightarrow S\mathrm{Po}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		isopolem	$$⊢H^{-1}{Isom}_{S,R}\left(B,A\right)\to \left(R\mathrm{Po}A\to S\mathrm{Po}B\right)$$
3	1 2	syl	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{Po}A\to S\mathrm{Po}B\right)$$
4		isopolem	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(S\mathrm{Po}B\to R\mathrm{Po}A\right)$$
5	3 4	impbid	$$⊢H{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{Po}A\leftrightarrow S\mathrm{Po}B\right)$$