Metamath Proof Explorer


Theorem isowe

Description: An isomorphism preserves the property of being a well-ordering. Proposition 6.32(3) of TakeutiZaring p. 33. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 18-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 isofr
 |-  ( H Isom R , S ( A , B ) -> ( R Fr A <-> S Fr B ) )
2 isoso
 |-  ( H Isom R , S ( A , B ) -> ( R Or A <-> S Or B ) )
3 1 2 anbi12d
 |-  ( H Isom R , S ( A , B ) -> ( ( R Fr A /\ R Or A ) <-> ( S Fr B /\ S Or B ) ) )
4 df-we
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )
5 df-we
 |-  ( S We B <-> ( S Fr B /\ S Or B ) )
6 3 4 5 3bitr4g
 |-  ( H Isom R , S ( A , B ) -> ( R We A <-> S We B ) )