Metamath Proof Explorer

Theorem soisoi

Description: Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion soisoi 
|- ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H Isom R , S ( A , B ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H : A -onto-> B )
2 fof 
 |-  ( H : A -onto-> B -> H : A --> B )
3 1 2 syl 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H : A --> B )
4 sotrieq 
 |-  ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( a = b <-> -. ( a R b \/ b R a ) ) )
5 4 con2bid 
 |-  ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( ( a R b \/ b R a ) <-> -. a = b ) )
6 5 ad4ant14 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( a R b \/ b R a ) <-> -. a = b ) )
7 simprr 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) )
8 breq1 
 |-  ( x = a -> ( x R y <-> a R y ) )
9 fveq2 
 |-  ( x = a -> ( H ` x ) = ( H ` a ) )
10 9 breq1d 
 |-  ( x = a -> ( ( H ` x ) S ( H ` y ) <-> ( H ` a ) S ( H ` y ) ) )
11 8 10 imbi12d 
 |-  ( x = a -> ( ( x R y -> ( H ` x ) S ( H ` y ) ) <-> ( a R y -> ( H ` a ) S ( H ` y ) ) ) )
12 breq2 
 |-  ( y = b -> ( a R y <-> a R b ) )
13 fveq2 
 |-  ( y = b -> ( H ` y ) = ( H ` b ) )
14 13 breq2d 
 |-  ( y = b -> ( ( H ` a ) S ( H ` y ) <-> ( H ` a ) S ( H ` b ) ) )
15 12 14 imbi12d 
 |-  ( y = b -> ( ( a R y -> ( H ` a ) S ( H ` y ) ) <-> ( a R b -> ( H ` a ) S ( H ` b ) ) ) )
16 11 15 rspc2va 
 |-  ( ( ( a e. A /\ b e. A ) /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) -> ( a R b -> ( H ` a ) S ( H ` b ) ) )
17 16 ancoms 
 |-  ( ( A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) /\ ( a e. A /\ b e. A ) ) -> ( a R b -> ( H ` a ) S ( H ` b ) ) )
18 7 17 sylan 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( a R b -> ( H ` a ) S ( H ` b ) ) )
19 simpllr 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> S Po B )
20 simplrl 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> H : A -onto-> B )
21 20 2 syl 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> H : A --> B )
22 simprr 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> b e. A )
23 21 22 ffvelcdmd 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( H ` b ) e. B )
24 poirr 
 |-  ( ( S Po B /\ ( H ` b ) e. B ) -> -. ( H ` b ) S ( H ` b ) )
25 breq1 
 |-  ( ( H ` a ) = ( H ` b ) -> ( ( H ` a ) S ( H ` b ) <-> ( H ` b ) S ( H ` b ) ) )
26 25 notbid 
 |-  ( ( H ` a ) = ( H ` b ) -> ( -. ( H ` a ) S ( H ` b ) <-> -. ( H ` b ) S ( H ` b ) ) )
27 24 26 syl5ibrcom 
 |-  ( ( S Po B /\ ( H ` b ) e. B ) -> ( ( H ` a ) = ( H ` b ) -> -. ( H ` a ) S ( H ` b ) ) )
28 19 23 27 syl2anc 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` a ) = ( H ` b ) -> -. ( H ` a ) S ( H ` b ) ) )
29 28 con2d 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` a ) S ( H ` b ) -> -. ( H ` a ) = ( H ` b ) ) )
30 18 29 syld 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( a R b -> -. ( H ` a ) = ( H ` b ) ) )
31 breq1 
 |-  ( x = b -> ( x R y <-> b R y ) )
32 fveq2 
 |-  ( x = b -> ( H ` x ) = ( H ` b ) )
33 32 breq1d 
 |-  ( x = b -> ( ( H ` x ) S ( H ` y ) <-> ( H ` b ) S ( H ` y ) ) )
34 31 33 imbi12d 
 |-  ( x = b -> ( ( x R y -> ( H ` x ) S ( H ` y ) ) <-> ( b R y -> ( H ` b ) S ( H ` y ) ) ) )
35 breq2 
 |-  ( y = a -> ( b R y <-> b R a ) )
36 fveq2 
 |-  ( y = a -> ( H ` y ) = ( H ` a ) )
37 36 breq2d 
 |-  ( y = a -> ( ( H ` b ) S ( H ` y ) <-> ( H ` b ) S ( H ` a ) ) )
38 35 37 imbi12d 
 |-  ( y = a -> ( ( b R y -> ( H ` b ) S ( H ` y ) ) <-> ( b R a -> ( H ` b ) S ( H ` a ) ) ) )
39 34 38 rspc2va 
 |-  ( ( ( b e. A /\ a e. A ) /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) -> ( b R a -> ( H ` b ) S ( H ` a ) ) )
40 39 ancoms 
 |-  ( ( A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) /\ ( b e. A /\ a e. A ) ) -> ( b R a -> ( H ` b ) S ( H ` a ) ) )
41 40 ancom2s 
 |-  ( ( A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) /\ ( a e. A /\ b e. A ) ) -> ( b R a -> ( H ` b ) S ( H ` a ) ) )
42 7 41 sylan 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( b R a -> ( H ` b ) S ( H ` a ) ) )
43 breq2 
 |-  ( ( H ` a ) = ( H ` b ) -> ( ( H ` b ) S ( H ` a ) <-> ( H ` b ) S ( H ` b ) ) )
44 43 notbid 
 |-  ( ( H ` a ) = ( H ` b ) -> ( -. ( H ` b ) S ( H ` a ) <-> -. ( H ` b ) S ( H ` b ) ) )
45 24 44 syl5ibrcom 
 |-  ( ( S Po B /\ ( H ` b ) e. B ) -> ( ( H ` a ) = ( H ` b ) -> -. ( H ` b ) S ( H ` a ) ) )
46 19 23 45 syl2anc 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` a ) = ( H ` b ) -> -. ( H ` b ) S ( H ` a ) ) )
47 46 con2d 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` b ) S ( H ` a ) -> -. ( H ` a ) = ( H ` b ) ) )
48 42 47 syld 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( b R a -> -. ( H ` a ) = ( H ` b ) ) )
49 30 48 jaod 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( a R b \/ b R a ) -> -. ( H ` a ) = ( H ` b ) ) )
50 6 49 sylbird 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( -. a = b -> -. ( H ` a ) = ( H ` b ) ) )
51 50 con4d 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` a ) = ( H ` b ) -> a = b ) )
52 51 ralrimivva 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> A. a e. A A. b e. A ( ( H ` a ) = ( H ` b ) -> a = b ) )
53 dff13 
 |-  ( H : A -1-1-> B <-> ( H : A --> B /\ A. a e. A A. b e. A ( ( H ` a ) = ( H ` b ) -> a = b ) ) )
54 3 52 53 sylanbrc 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H : A -1-1-> B )
55 df-f1o 
 |-  ( H : A -1-1-onto-> B <-> ( H : A -1-1-> B /\ H : A -onto-> B ) )
56 54 1 55 sylanbrc 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H : A -1-1-onto-> B )
57 sotric 
 |-  ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( a R b <-> -. ( a = b \/ b R a ) ) )
58 57 con2bid 
 |-  ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( ( a = b \/ b R a ) <-> -. a R b ) )
59 58 ad4ant14 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( a = b \/ b R a ) <-> -. a R b ) )
60 fveq2 
 |-  ( a = b -> ( H ` a ) = ( H ` b ) )
61 60 breq1d 
 |-  ( a = b -> ( ( H ` a ) S ( H ` b ) <-> ( H ` b ) S ( H ` b ) ) )
62 61 notbid 
 |-  ( a = b -> ( -. ( H ` a ) S ( H ` b ) <-> -. ( H ` b ) S ( H ` b ) ) )
63 24 62 syl5ibrcom 
 |-  ( ( S Po B /\ ( H ` b ) e. B ) -> ( a = b -> -. ( H ` a ) S ( H ` b ) ) )
64 19 23 63 syl2anc 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( a = b -> -. ( H ` a ) S ( H ` b ) ) )
65 simprl 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> a e. A )
66 21 65 ffvelcdmd 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( H ` a ) e. B )
67 po2nr 
 |-  ( ( S Po B /\ ( ( H ` b ) e. B /\ ( H ` a ) e. B ) ) -> -. ( ( H ` b ) S ( H ` a ) /\ ( H ` a ) S ( H ` b ) ) )
68 imnan 
 |-  ( ( ( H ` b ) S ( H ` a ) -> -. ( H ` a ) S ( H ` b ) ) <-> -. ( ( H ` b ) S ( H ` a ) /\ ( H ` a ) S ( H ` b ) ) )
69 67 68 sylibr 
 |-  ( ( S Po B /\ ( ( H ` b ) e. B /\ ( H ` a ) e. B ) ) -> ( ( H ` b ) S ( H ` a ) -> -. ( H ` a ) S ( H ` b ) ) )
70 19 23 66 69 syl12anc 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( H ` b ) S ( H ` a ) -> -. ( H ` a ) S ( H ` b ) ) )
71 42 70 syld 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( b R a -> -. ( H ` a ) S ( H ` b ) ) )
72 64 71 jaod 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( ( a = b \/ b R a ) -> -. ( H ` a ) S ( H ` b ) ) )
73 59 72 sylbird 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( -. a R b -> -. ( H ` a ) S ( H ` b ) ) )
74 18 73 impcon4bid 
 |-  ( ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) /\ ( a e. A /\ b e. A ) ) -> ( a R b <-> ( H ` a ) S ( H ` b ) ) )
75 74 ralrimivva 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) )
76 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
77 56 75 76 sylanbrc 
 |-  ( ( ( R Or A /\ S Po B ) /\ ( H : A -onto-> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) -> H Isom R , S ( A , B ) )