Theorem isofr

Description: An isomorphism preserves well-foundedness. Proposition 6.32(1) of TakeutiZaring p. 33. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 18-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isocnv	|- ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )
2		id	|- ( `' H Isom S , R ( B , A ) -> `' H Isom S , R ( B , A ) )
3		isof1o	|- ( `' H Isom S , R ( B , A ) -> `' H : B -1-1-onto-> A )
4		f1ofun	|- ( `' H : B -1-1-onto-> A -> Fun `' H )
5		vex	|- x e. _V
6	5	funimaex	|- ( Fun `' H -> ( `' H " x ) e. _V )
7	3 4 6	3syl	|- ( `' H Isom S , R ( B , A ) -> ( `' H " x ) e. _V )
8	2 7	isofrlem	|- ( `' H Isom S , R ( B , A ) -> ( R Fr A -> S Fr B ) )
9	1 8	syl	|- ( H Isom R , S ( A , B ) -> ( R Fr A -> S Fr B ) )
10		id	|- ( H Isom R , S ( A , B ) -> H Isom R , S ( A , B ) )
11		isof1o	|- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
12		f1ofun	|- ( H : A -1-1-onto-> B -> Fun H )
13	5	funimaex	|- ( Fun H -> ( H " x ) e. _V )
14	11 12 13	3syl	|- ( H Isom R , S ( A , B ) -> ( H " x ) e. _V )
15	10 14	isofrlem	|- ( H Isom R , S ( A , B ) -> ( S Fr B -> R Fr A ) )
16	9 15	impbid	|- ( H Isom R , S ( A , B ) -> ( R Fr A <-> S Fr B ) )