Metamath Proof Explorer


Theorem isowe

Description: An isomorphism preserves 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