Metamath Proof Explorer

Theorem f1oiso2

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . (Contributed by Mario Carneiro, 9-Mar-2013)

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

Proof

Step Hyp Ref Expression
1 f1oiso2.1 
 |-  S = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) }
2 f1ocnvdm 
 |-  ( ( H : A -1-1-onto-> B /\ x e. B ) -> ( `' H ` x ) e. A )
3 2 adantrr 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) ) -> ( `' H ` x ) e. A )
4 3 3adant3 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> ( `' H ` x ) e. A )
5 f1ocnvdm 
 |-  ( ( H : A -1-1-onto-> B /\ y e. B ) -> ( `' H ` y ) e. A )
6 5 adantrl 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) ) -> ( `' H ` y ) e. A )
7 6 3adant3 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> ( `' H ` y ) e. A )
8 f1ocnvfv2 
 |-  ( ( H : A -1-1-onto-> B /\ x e. B ) -> ( H ` ( `' H ` x ) ) = x )
9 8 eqcomd 
 |-  ( ( H : A -1-1-onto-> B /\ x e. B ) -> x = ( H ` ( `' H ` x ) ) )
10 f1ocnvfv2 
 |-  ( ( H : A -1-1-onto-> B /\ y e. B ) -> ( H ` ( `' H ` y ) ) = y )
11 10 eqcomd 
 |-  ( ( H : A -1-1-onto-> B /\ y e. B ) -> y = ( H ` ( `' H ` y ) ) )
12 9 11 anim12dan 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) ) -> ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` ( `' H ` y ) ) ) )
13 12 3adant3 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` ( `' H ` y ) ) ) )
14 simp3 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> ( `' H ` x ) R ( `' H ` y ) )
15 fveq2 
 |-  ( w = ( `' H ` y ) -> ( H ` w ) = ( H ` ( `' H ` y ) ) )
16 15 eqeq2d 
 |-  ( w = ( `' H ` y ) -> ( y = ( H ` w ) <-> y = ( H ` ( `' H ` y ) ) ) )
17 16 anbi2d 
 |-  ( w = ( `' H ` y ) -> ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) <-> ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` ( `' H ` y ) ) ) ) )
18 breq2 
 |-  ( w = ( `' H ` y ) -> ( ( `' H ` x ) R w <-> ( `' H ` x ) R ( `' H ` y ) ) )
19 17 18 anbi12d 
 |-  ( w = ( `' H ` y ) -> ( ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) <-> ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` ( `' H ` y ) ) ) /\ ( `' H ` x ) R ( `' H ` y ) ) ) )
20 19 rspcev 
 |-  ( ( ( `' H ` y ) e. A /\ ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` ( `' H ` y ) ) ) /\ ( `' H ` x ) R ( `' H ` y ) ) ) -> E. w e. A ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) )
21 7 13 14 20 syl12anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> E. w e. A ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) )
22 fveq2 
 |-  ( z = ( `' H ` x ) -> ( H ` z ) = ( H ` ( `' H ` x ) ) )
23 22 eqeq2d 
 |-  ( z = ( `' H ` x ) -> ( x = ( H ` z ) <-> x = ( H ` ( `' H ` x ) ) ) )
24 23 anbi1d 
 |-  ( z = ( `' H ` x ) -> ( ( x = ( H ` z ) /\ y = ( H ` w ) ) <-> ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) ) )
25 breq1 
 |-  ( z = ( `' H ` x ) -> ( z R w <-> ( `' H ` x ) R w ) )
26 24 25 anbi12d 
 |-  ( z = ( `' H ` x ) -> ( ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) <-> ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) ) )
27 26 rexbidv 
 |-  ( z = ( `' H ` x ) -> ( E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) <-> E. w e. A ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) ) )
28 27 rspcev 
 |-  ( ( ( `' H ` x ) e. A /\ E. w e. A ( ( x = ( H ` ( `' H ` x ) ) /\ y = ( H ` w ) ) /\ ( `' H ` x ) R w ) ) -> E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) )
29 4 21 28 syl2anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) )
30 29 3expib 
 |-  ( H : A -1-1-onto-> B -> ( ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) -> E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) )
31 simp3ll 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> x = ( H ` z ) )
32 simp1 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> H : A -1-1-onto-> B )
33 simp2l 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> z e. A )
34 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
35 34 ffvelrnda 
 |-  ( ( H : A -1-1-onto-> B /\ z e. A ) -> ( H ` z ) e. B )
36 32 33 35 syl2anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( H ` z ) e. B )
37 31 36 eqeltrd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> x e. B )
38 simp3lr 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> y = ( H ` w ) )
39 simp2r 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> w e. A )
40 34 ffvelrnda 
 |-  ( ( H : A -1-1-onto-> B /\ w e. A ) -> ( H ` w ) e. B )
41 32 39 40 syl2anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( H ` w ) e. B )
42 38 41 eqeltrd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> y e. B )
43 simp3r 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> z R w )
44 31 eqcomd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( H ` z ) = x )
45 f1ocnvfv 
 |-  ( ( H : A -1-1-onto-> B /\ z e. A ) -> ( ( H ` z ) = x -> ( `' H ` x ) = z ) )
46 32 33 45 syl2anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( ( H ` z ) = x -> ( `' H ` x ) = z ) )
47 44 46 mpd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( `' H ` x ) = z )
48 38 eqcomd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( H ` w ) = y )
49 f1ocnvfv 
 |-  ( ( H : A -1-1-onto-> B /\ w e. A ) -> ( ( H ` w ) = y -> ( `' H ` y ) = w ) )
50 32 39 49 syl2anc 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( ( H ` w ) = y -> ( `' H ` y ) = w ) )
51 48 50 mpd 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( `' H ` y ) = w )
52 43 47 51 3brtr4d 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( `' H ` x ) R ( `' H ` y ) )
53 37 42 52 jca31 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. A /\ w e. A ) /\ ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) -> ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) )
54 53 3exp 
 |-  ( H : A -1-1-onto-> B -> ( ( z e. A /\ w e. A ) -> ( ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) -> ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) ) ) )
55 54 rexlimdvv 
 |-  ( H : A -1-1-onto-> B -> ( E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) -> ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) ) )
56 30 55 impbid 
 |-  ( H : A -1-1-onto-> B -> ( ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) <-> E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) ) )
57 56 opabbidv 
 |-  ( H : A -1-1-onto-> B -> { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) } = { <. x , y >. | E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) } )
58 1 57 syl5eq 
 |-  ( H : A -1-1-onto-> B -> S = { <. x , y >. | E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) } )
59 f1oiso 
 |-  ( ( H : A -1-1-onto-> B /\ S = { <. x , y >. | E. z e. A E. w e. A ( ( x = ( H ` z ) /\ y = ( H ` w ) ) /\ z R w ) } ) -> H Isom R , S ( A , B ) )
60 58 59 mpdan 
 |-  ( H : A -1-1-onto-> B -> H Isom R , S ( A , B ) )