This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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