Theorem isopo

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

	Ref	Expression
Assertion	isopo	|- ( H Isom R , S ( A , B ) -> ( R Po A <-> S Po B ) )

Proof

Step	Hyp	Ref	Expression
1		isocnv	|- ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )
2		isopolem	|- ( `' H Isom S , R ( B , A ) -> ( R Po A -> S Po B ) )
3	1 2	syl	|- ( H Isom R , S ( A , B ) -> ( R Po A -> S Po B ) )
4		isopolem	|- ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )
5	3 4	impbid	|- ( H Isom R , S ( A , B ) -> ( R Po A <-> S Po B ) )