Metamath Proof Explorer

Theorem f1oiso

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . Proposition 6.33 of TakeutiZaring p. 34. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion f1oiso 
|- ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> H Isom R , S ( A , B ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> H : A -1-1-onto-> B )
2 f1of1 
 |-  ( H : A -1-1-onto-> B -> H : A -1-1-> B )
3 df-br 
 |-  ( ( H ` v ) S ( H ` u ) <-> <. ( H ` v ) , ( H ` u ) >. e. S )
4 eleq2 
 |-  ( S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } -> ( <. ( H ` v ) , ( H ` u ) >. e. S <-> <. ( H ` v ) , ( H ` u ) >. e. { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) )
5 fvex 
 |-  ( H ` v ) e. _V
6 fvex 
 |-  ( H ` u ) e. _V
7 eqeq1 
 |-  ( z = ( H ` v ) -> ( z = ( H ` x ) <-> ( H ` v ) = ( H ` x ) ) )
8 7 anbi1d 
 |-  ( z = ( H ` v ) -> ( ( z = ( H ` x ) /\ w = ( H ` y ) ) <-> ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) ) )
9 8 anbi1d 
 |-  ( z = ( H ` v ) -> ( ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) <-> ( ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) ) )
10 9 2rexbidv 
 |-  ( z = ( H ` v ) -> ( E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) <-> E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) ) )
11 eqeq1 
 |-  ( w = ( H ` u ) -> ( w = ( H ` y ) <-> ( H ` u ) = ( H ` y ) ) )
12 11 anbi2d 
 |-  ( w = ( H ` u ) -> ( ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) <-> ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) ) )
13 12 anbi1d 
 |-  ( w = ( H ` u ) -> ( ( ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) <-> ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) ) )
14 13 2rexbidv 
 |-  ( w = ( H ` u ) -> ( E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) <-> E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) ) )
15 5 6 10 14 opelopab 
 |-  ( <. ( H ` v ) , ( H ` u ) >. e. { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } <-> E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) )
16 anass 
 |-  ( ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> ( ( H ` v ) = ( H ` x ) /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) )
17 f1fveq 
 |-  ( ( H : A -1-1-> B /\ ( v e. A /\ x e. A ) ) -> ( ( H ` v ) = ( H ` x ) <-> v = x ) )
18 equcom 
 |-  ( v = x <-> x = v )
19 17 18 bitrdi 
 |-  ( ( H : A -1-1-> B /\ ( v e. A /\ x e. A ) ) -> ( ( H ` v ) = ( H ` x ) <-> x = v ) )
20 19 anassrs 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ x e. A ) -> ( ( H ` v ) = ( H ` x ) <-> x = v ) )
21 20 anbi1d 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ x e. A ) -> ( ( ( H ` v ) = ( H ` x ) /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) <-> ( x = v /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) ) )
22 16 21 syl5bb 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ x e. A ) -> ( ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> ( x = v /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) ) )
23 22 rexbidv 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ x e. A ) -> ( E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> E. y e. A ( x = v /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) ) )
24 r19.42v 
 |-  ( E. y e. A ( x = v /\ ( ( H ` u ) = ( H ` y ) /\ x R y ) ) <-> ( x = v /\ E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) ) )
25 23 24 bitrdi 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ x e. A ) -> ( E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> ( x = v /\ E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) ) ) )
26 25 rexbidva 
 |-  ( ( H : A -1-1-> B /\ v e. A ) -> ( E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> E. x e. A ( x = v /\ E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) ) ) )
27 breq1 
 |-  ( x = v -> ( x R y <-> v R y ) )
28 27 anbi2d 
 |-  ( x = v -> ( ( ( H ` u ) = ( H ` y ) /\ x R y ) <-> ( ( H ` u ) = ( H ` y ) /\ v R y ) ) )
29 28 rexbidv 
 |-  ( x = v -> ( E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) <-> E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) ) )
30 29 ceqsrexv 
 |-  ( v e. A -> ( E. x e. A ( x = v /\ E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) ) <-> E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) ) )
31 30 adantl 
 |-  ( ( H : A -1-1-> B /\ v e. A ) -> ( E. x e. A ( x = v /\ E. y e. A ( ( H ` u ) = ( H ` y ) /\ x R y ) ) <-> E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) ) )
32 26 31 bitrd 
 |-  ( ( H : A -1-1-> B /\ v e. A ) -> ( E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) ) )
33 f1fveq 
 |-  ( ( H : A -1-1-> B /\ ( u e. A /\ y e. A ) ) -> ( ( H ` u ) = ( H ` y ) <-> u = y ) )
34 equcom 
 |-  ( u = y <-> y = u )
35 33 34 bitrdi 
 |-  ( ( H : A -1-1-> B /\ ( u e. A /\ y e. A ) ) -> ( ( H ` u ) = ( H ` y ) <-> y = u ) )
36 35 anassrs 
 |-  ( ( ( H : A -1-1-> B /\ u e. A ) /\ y e. A ) -> ( ( H ` u ) = ( H ` y ) <-> y = u ) )
37 36 anbi1d 
 |-  ( ( ( H : A -1-1-> B /\ u e. A ) /\ y e. A ) -> ( ( ( H ` u ) = ( H ` y ) /\ v R y ) <-> ( y = u /\ v R y ) ) )
38 37 rexbidva 
 |-  ( ( H : A -1-1-> B /\ u e. A ) -> ( E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) <-> E. y e. A ( y = u /\ v R y ) ) )
39 breq2 
 |-  ( y = u -> ( v R y <-> v R u ) )
40 39 ceqsrexv 
 |-  ( u e. A -> ( E. y e. A ( y = u /\ v R y ) <-> v R u ) )
41 40 adantl 
 |-  ( ( H : A -1-1-> B /\ u e. A ) -> ( E. y e. A ( y = u /\ v R y ) <-> v R u ) )
42 38 41 bitrd 
 |-  ( ( H : A -1-1-> B /\ u e. A ) -> ( E. y e. A ( ( H ` u ) = ( H ` y ) /\ v R y ) <-> v R u ) )
43 32 42 sylan9bb 
 |-  ( ( ( H : A -1-1-> B /\ v e. A ) /\ ( H : A -1-1-> B /\ u e. A ) ) -> ( E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> v R u ) )
44 43 anandis 
 |-  ( ( H : A -1-1-> B /\ ( v e. A /\ u e. A ) ) -> ( E. x e. A E. y e. A ( ( ( H ` v ) = ( H ` x ) /\ ( H ` u ) = ( H ` y ) ) /\ x R y ) <-> v R u ) )
45 15 44 syl5bb 
 |-  ( ( H : A -1-1-> B /\ ( v e. A /\ u e. A ) ) -> ( <. ( H ` v ) , ( H ` u ) >. e. { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } <-> v R u ) )
46 4 45 sylan9bbr 
 |-  ( ( ( H : A -1-1-> B /\ ( v e. A /\ u e. A ) ) /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> ( <. ( H ` v ) , ( H ` u ) >. e. S <-> v R u ) )
47 46 an32s 
 |-  ( ( ( H : A -1-1-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) /\ ( v e. A /\ u e. A ) ) -> ( <. ( H ` v ) , ( H ` u ) >. e. S <-> v R u ) )
48 3 47 bitr2id 
 |-  ( ( ( H : A -1-1-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) /\ ( v e. A /\ u e. A ) ) -> ( v R u <-> ( H ` v ) S ( H ` u ) ) )
49 48 ralrimivva 
 |-  ( ( H : A -1-1-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> A. v e. A A. u e. A ( v R u <-> ( H ` v ) S ( H ` u ) ) )
50 2 49 sylan 
 |-  ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> A. v e. A A. u e. A ( v R u <-> ( H ` v ) S ( H ` u ) ) )
51 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. v e. A A. u e. A ( v R u <-> ( H ` v ) S ( H ` u ) ) ) )
52 1 50 51 sylanbrc 
 |-  ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> H Isom R , S ( A , B ) )