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