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