Metamath Proof Explorer

Theorem soisores

Description: Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Assertion soisores 
|- ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> ( ( F |` A ) Isom R , S ( A , ( F " A ) ) <-> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 isorel 
 |-  ( ( ( F |` A ) Isom R , S ( A , ( F " A ) ) /\ ( x e. A /\ y e. A ) ) -> ( x R y <-> ( ( F |` A ) ` x ) S ( ( F |` A ) ` y ) ) )
2 fvres 
 |-  ( x e. A -> ( ( F |` A ) ` x ) = ( F ` x ) )
3 fvres 
 |-  ( y e. A -> ( ( F |` A ) ` y ) = ( F ` y ) )
4 2 3 breqan12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( ( F |` A ) ` x ) S ( ( F |` A ) ` y ) <-> ( F ` x ) S ( F ` y ) ) )
5 4 adantl 
 |-  ( ( ( F |` A ) Isom R , S ( A , ( F " A ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( ( F |` A ) ` x ) S ( ( F |` A ) ` y ) <-> ( F ` x ) S ( F ` y ) ) )
6 1 5 bitrd 
 |-  ( ( ( F |` A ) Isom R , S ( A , ( F " A ) ) /\ ( x e. A /\ y e. A ) ) -> ( x R y <-> ( F ` x ) S ( F ` y ) ) )
7 6 biimpd 
 |-  ( ( ( F |` A ) Isom R , S ( A , ( F " A ) ) /\ ( x e. A /\ y e. A ) ) -> ( x R y -> ( F ` x ) S ( F ` y ) ) )
8 7 ralrimivva 
 |-  ( ( F |` A ) Isom R , S ( A , ( F " A ) ) -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
9 ffn 
 |-  ( F : B --> C -> F Fn B )
10 9 ad2antrl 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> F Fn B )
11 simprr 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> A C_ B )
12 fnssres 
 |-  ( ( F Fn B /\ A C_ B ) -> ( F |` A ) Fn A )
13 10 11 12 syl2anc 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> ( F |` A ) Fn A )
14 13 3adant3 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ( F |` A ) Fn A )
15 df-ima 
 |-  ( F " A ) = ran ( F |` A )
16 15 eqcomi 
 |-  ran ( F |` A ) = ( F " A )
17 16 a1i 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ran ( F |` A ) = ( F " A ) )
18 fvres 
 |-  ( z e. A -> ( ( F |` A ) ` z ) = ( F ` z ) )
19 fvres 
 |-  ( w e. A -> ( ( F |` A ) ` w ) = ( F ` w ) )
20 18 19 eqeqan12d 
 |-  ( ( z e. A /\ w e. A ) -> ( ( ( F |` A ) ` z ) = ( ( F |` A ) ` w ) <-> ( F ` z ) = ( F ` w ) ) )
21 20 adantl 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( ( F |` A ) ` z ) = ( ( F |` A ) ` w ) <-> ( F ` z ) = ( F ` w ) ) )
22 simprl 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> z e. A )
23 simprr 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> w e. A )
24 simpl3 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
25 breq1 
 |-  ( x = z -> ( x R y <-> z R y ) )
26 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
27 26 breq1d 
 |-  ( x = z -> ( ( F ` x ) S ( F ` y ) <-> ( F ` z ) S ( F ` y ) ) )
28 25 27 imbi12d 
 |-  ( x = z -> ( ( x R y -> ( F ` x ) S ( F ` y ) ) <-> ( z R y -> ( F ` z ) S ( F ` y ) ) ) )
29 breq2 
 |-  ( y = w -> ( z R y <-> z R w ) )
30 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
31 30 breq2d 
 |-  ( y = w -> ( ( F ` z ) S ( F ` y ) <-> ( F ` z ) S ( F ` w ) ) )
32 29 31 imbi12d 
 |-  ( y = w -> ( ( z R y -> ( F ` z ) S ( F ` y ) ) <-> ( z R w -> ( F ` z ) S ( F ` w ) ) ) )
33 28 32 rspc2va 
 |-  ( ( ( z e. A /\ w e. A ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ( z R w -> ( F ` z ) S ( F ` w ) ) )
34 22 23 24 33 syl21anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z R w -> ( F ` z ) S ( F ` w ) ) )
35 breq1 
 |-  ( x = w -> ( x R y <-> w R y ) )
36 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
37 36 breq1d 
 |-  ( x = w -> ( ( F ` x ) S ( F ` y ) <-> ( F ` w ) S ( F ` y ) ) )
38 35 37 imbi12d 
 |-  ( x = w -> ( ( x R y -> ( F ` x ) S ( F ` y ) ) <-> ( w R y -> ( F ` w ) S ( F ` y ) ) ) )
39 breq2 
 |-  ( y = z -> ( w R y <-> w R z ) )
40 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
41 40 breq2d 
 |-  ( y = z -> ( ( F ` w ) S ( F ` y ) <-> ( F ` w ) S ( F ` z ) ) )
42 39 41 imbi12d 
 |-  ( y = z -> ( ( w R y -> ( F ` w ) S ( F ` y ) ) <-> ( w R z -> ( F ` w ) S ( F ` z ) ) ) )
43 38 42 rspc2va 
 |-  ( ( ( w e. A /\ z e. A ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ( w R z -> ( F ` w ) S ( F ` z ) ) )
44 23 22 24 43 syl21anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( w R z -> ( F ` w ) S ( F ` z ) ) )
45 34 44 orim12d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( z R w \/ w R z ) -> ( ( F ` z ) S ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
46 45 con3d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( -. ( ( F ` z ) S ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) -> -. ( z R w \/ w R z ) ) )
47 simpl1r 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> S Or C )
48 simpl2l 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> F : B --> C )
49 simpl2r 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> A C_ B )
50 49 22 sseldd 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> z e. B )
51 48 50 ffvelrnd 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( F ` z ) e. C )
52 49 23 sseldd 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> w e. B )
53 48 52 ffvelrnd 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( F ` w ) e. C )
54 sotrieq 
 |-  ( ( S Or C /\ ( ( F ` z ) e. C /\ ( F ` w ) e. C ) ) -> ( ( F ` z ) = ( F ` w ) <-> -. ( ( F ` z ) S ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
55 47 51 53 54 syl12anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) = ( F ` w ) <-> -. ( ( F ` z ) S ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
56 simpl1l 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> R Or B )
57 sotrieq 
 |-  ( ( R Or B /\ ( z e. B /\ w e. B ) ) -> ( z = w <-> -. ( z R w \/ w R z ) ) )
58 56 50 52 57 syl12anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z = w <-> -. ( z R w \/ w R z ) ) )
59 46 55 58 3imtr4d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
60 21 59 sylbid 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( ( F |` A ) ` z ) = ( ( F |` A ) ` w ) -> z = w ) )
61 60 ralrimivva 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> A. z e. A A. w e. A ( ( ( F |` A ) ` z ) = ( ( F |` A ) ` w ) -> z = w ) )
62 dff1o6 
 |-  ( ( F |` A ) : A -1-1-onto-> ( F " A ) <-> ( ( F |` A ) Fn A /\ ran ( F |` A ) = ( F " A ) /\ A. z e. A A. w e. A ( ( ( F |` A ) ` z ) = ( ( F |` A ) ` w ) -> z = w ) ) )
63 14 17 61 62 syl3anbrc 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
64 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
65 64 a1i 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z = w -> ( F ` z ) = ( F ` w ) ) )
66 65 44 orim12d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( z = w \/ w R z ) -> ( ( F ` z ) = ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
67 66 con3d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( -. ( ( F ` z ) = ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) -> -. ( z = w \/ w R z ) ) )
68 sotric 
 |-  ( ( S Or C /\ ( ( F ` z ) e. C /\ ( F ` w ) e. C ) ) -> ( ( F ` z ) S ( F ` w ) <-> -. ( ( F ` z ) = ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
69 47 51 53 68 syl12anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) S ( F ` w ) <-> -. ( ( F ` z ) = ( F ` w ) \/ ( F ` w ) S ( F ` z ) ) ) )
70 sotric 
 |-  ( ( R Or B /\ ( z e. B /\ w e. B ) ) -> ( z R w <-> -. ( z = w \/ w R z ) ) )
71 56 50 52 70 syl12anc 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z R w <-> -. ( z = w \/ w R z ) ) )
72 67 69 71 3imtr4d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) S ( F ` w ) -> z R w ) )
73 34 72 impbid 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z R w <-> ( F ` z ) S ( F ` w ) ) )
74 18 19 breqan12d 
 |-  ( ( z e. A /\ w e. A ) -> ( ( ( F |` A ) ` z ) S ( ( F |` A ) ` w ) <-> ( F ` z ) S ( F ` w ) ) )
75 74 adantl 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( ( F |` A ) ` z ) S ( ( F |` A ) ` w ) <-> ( F ` z ) S ( F ` w ) ) )
76 73 75 bitr4d 
 |-  ( ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z R w <-> ( ( F |` A ) ` z ) S ( ( F |` A ) ` w ) ) )
77 76 ralrimivva 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> A. z e. A A. w e. A ( z R w <-> ( ( F |` A ) ` z ) S ( ( F |` A ) ` w ) ) )
78 df-isom 
 |-  ( ( F |` A ) Isom R , S ( A , ( F " A ) ) <-> ( ( F |` A ) : A -1-1-onto-> ( F " A ) /\ A. z e. A A. w e. A ( z R w <-> ( ( F |` A ) ` z ) S ( ( F |` A ) ` w ) ) ) )
79 63 77 78 sylanbrc 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) /\ A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) -> ( F |` A ) Isom R , S ( A , ( F " A ) ) )
80 79 3expia 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> ( A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) -> ( F |` A ) Isom R , S ( A , ( F " A ) ) ) )
81 8 80 impbid2 
 |-  ( ( ( R Or B /\ S Or C ) /\ ( F : B --> C /\ A C_ B ) ) -> ( ( F |` A ) Isom R , S ( A , ( F " A ) ) <-> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) ) )