Metamath Proof Explorer


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 ) )