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

Metamath Proof Explorer

Theorem f1owe

Description: Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997)

Ref Expression
Hypothesis f1owe.1 
|- R = { <. x , y >. | ( F ` x ) S ( F ` y ) }
Assertion f1owe 
|- ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )

Proof

Step Hyp Ref Expression
1 f1owe.1 
 |-  R = { <. x , y >. | ( F ` x ) S ( F ` y ) }
2 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
3 2 breq1d 
 |-  ( x = z -> ( ( F ` x ) S ( F ` y ) <-> ( F ` z ) S ( F ` y ) ) )
4 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
5 4 breq2d 
 |-  ( y = w -> ( ( F ` z ) S ( F ` y ) <-> ( F ` z ) S ( F ` w ) ) )
6 3 5 1 brabg 
 |-  ( ( z e. A /\ w e. A ) -> ( z R w <-> ( F ` z ) S ( F ` w ) ) )
7 6 rgen2 
 |-  A. z e. A A. w e. A ( z R w <-> ( F ` z ) S ( F ` w ) )
8 df-isom 
 |-  ( F Isom R , S ( A , B ) <-> ( F : A -1-1-onto-> B /\ A. z e. A A. w e. A ( z R w <-> ( F ` z ) S ( F ` w ) ) ) )
9 isowe 
 |-  ( F Isom R , S ( A , B ) -> ( R We A <-> S We B ) )
10 8 9 sylbir 
 |-  ( ( F : A -1-1-onto-> B /\ A. z e. A A. w e. A ( z R w <-> ( F ` z ) S ( F ` w ) ) ) -> ( R We A <-> S We B ) )
11 7 10 mpan2 
 |-  ( F : A -1-1-onto-> B -> ( R We A <-> S We B ) )
12 11 biimprd 
 |-  ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )