Metamath Proof Explorer

Theorem isopolem

Description: Lemma for isopo . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion isopolem 
|- ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )

Proof

Step Hyp Ref Expression
1 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
2 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
3 ffvelrn 
 |-  ( ( H : A --> B /\ d e. A ) -> ( H ` d ) e. B )
4 3 ex 
 |-  ( H : A --> B -> ( d e. A -> ( H ` d ) e. B ) )
5 ffvelrn 
 |-  ( ( H : A --> B /\ e e. A ) -> ( H ` e ) e. B )
6 5 ex 
 |-  ( H : A --> B -> ( e e. A -> ( H ` e ) e. B ) )
7 ffvelrn 
 |-  ( ( H : A --> B /\ f e. A ) -> ( H ` f ) e. B )
8 7 ex 
 |-  ( H : A --> B -> ( f e. A -> ( H ` f ) e. B ) )
9 4 6 8 3anim123d 
 |-  ( H : A --> B -> ( ( d e. A /\ e e. A /\ f e. A ) -> ( ( H ` d ) e. B /\ ( H ` e ) e. B /\ ( H ` f ) e. B ) ) )
10 1 2 9 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( ( d e. A /\ e e. A /\ f e. A ) -> ( ( H ` d ) e. B /\ ( H ` e ) e. B /\ ( H ` f ) e. B ) ) )
11 10 imp 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( ( H ` d ) e. B /\ ( H ` e ) e. B /\ ( H ` f ) e. B ) )
12 breq12 
 |-  ( ( a = ( H ` d ) /\ a = ( H ` d ) ) -> ( a S a <-> ( H ` d ) S ( H ` d ) ) )
13 12 anidms 
 |-  ( a = ( H ` d ) -> ( a S a <-> ( H ` d ) S ( H ` d ) ) )
14 13 notbid 
 |-  ( a = ( H ` d ) -> ( -. a S a <-> -. ( H ` d ) S ( H ` d ) ) )
15 breq1 
 |-  ( a = ( H ` d ) -> ( a S b <-> ( H ` d ) S b ) )
16 15 anbi1d 
 |-  ( a = ( H ` d ) -> ( ( a S b /\ b S c ) <-> ( ( H ` d ) S b /\ b S c ) ) )
17 breq1 
 |-  ( a = ( H ` d ) -> ( a S c <-> ( H ` d ) S c ) )
18 16 17 imbi12d 
 |-  ( a = ( H ` d ) -> ( ( ( a S b /\ b S c ) -> a S c ) <-> ( ( ( H ` d ) S b /\ b S c ) -> ( H ` d ) S c ) ) )
19 14 18 anbi12d 
 |-  ( a = ( H ` d ) -> ( ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) <-> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S b /\ b S c ) -> ( H ` d ) S c ) ) ) )
20 breq2 
 |-  ( b = ( H ` e ) -> ( ( H ` d ) S b <-> ( H ` d ) S ( H ` e ) ) )
21 breq1 
 |-  ( b = ( H ` e ) -> ( b S c <-> ( H ` e ) S c ) )
22 20 21 anbi12d 
 |-  ( b = ( H ` e ) -> ( ( ( H ` d ) S b /\ b S c ) <-> ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) ) )
23 22 imbi1d 
 |-  ( b = ( H ` e ) -> ( ( ( ( H ` d ) S b /\ b S c ) -> ( H ` d ) S c ) <-> ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) -> ( H ` d ) S c ) ) )
24 23 anbi2d 
 |-  ( b = ( H ` e ) -> ( ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S b /\ b S c ) -> ( H ` d ) S c ) ) <-> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) -> ( H ` d ) S c ) ) ) )
25 breq2 
 |-  ( c = ( H ` f ) -> ( ( H ` e ) S c <-> ( H ` e ) S ( H ` f ) ) )
26 25 anbi2d 
 |-  ( c = ( H ` f ) -> ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) <-> ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) ) )
27 breq2 
 |-  ( c = ( H ` f ) -> ( ( H ` d ) S c <-> ( H ` d ) S ( H ` f ) ) )
28 26 27 imbi12d 
 |-  ( c = ( H ` f ) -> ( ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) -> ( H ` d ) S c ) <-> ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) )
29 28 anbi2d 
 |-  ( c = ( H ` f ) -> ( ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S c ) -> ( H ` d ) S c ) ) <-> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) ) )
30 19 24 29 rspc3v 
 |-  ( ( ( H ` d ) e. B /\ ( H ` e ) e. B /\ ( H ` f ) e. B ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) ) )
31 11 30 syl 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) ) )
32 simpl 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> H Isom R , S ( A , B ) )
33 simpr1 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> d e. A )
34 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ d e. A ) ) -> ( d R d <-> ( H ` d ) S ( H ` d ) ) )
35 32 33 33 34 syl12anc 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( d R d <-> ( H ` d ) S ( H ` d ) ) )
36 35 notbid 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( -. d R d <-> -. ( H ` d ) S ( H ` d ) ) )
37 simpr2 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> e e. A )
38 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A ) ) -> ( d R e <-> ( H ` d ) S ( H ` e ) ) )
39 32 33 37 38 syl12anc 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( d R e <-> ( H ` d ) S ( H ` e ) ) )
40 simpr3 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> f e. A )
41 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( e e. A /\ f e. A ) ) -> ( e R f <-> ( H ` e ) S ( H ` f ) ) )
42 32 37 40 41 syl12anc 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( e R f <-> ( H ` e ) S ( H ` f ) ) )
43 39 42 anbi12d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( ( d R e /\ e R f ) <-> ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) ) )
44 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ f e. A ) ) -> ( d R f <-> ( H ` d ) S ( H ` f ) ) )
45 32 33 40 44 syl12anc 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( d R f <-> ( H ` d ) S ( H ` f ) ) )
46 43 45 imbi12d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( ( ( d R e /\ e R f ) -> d R f ) <-> ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) )
47 36 46 anbi12d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) <-> ( -. ( H ` d ) S ( H ` d ) /\ ( ( ( H ` d ) S ( H ` e ) /\ ( H ` e ) S ( H ` f ) ) -> ( H ` d ) S ( H ` f ) ) ) ) )
48 31 47 sylibrd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) ) )
49 48 ex 
 |-  ( H Isom R , S ( A , B ) -> ( ( d e. A /\ e e. A /\ f e. A ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) ) ) )
50 49 com23 
 |-  ( H Isom R , S ( A , B ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> ( ( d e. A /\ e e. A /\ f e. A ) -> ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) ) ) )
51 50 imp31 
 |-  ( ( ( H Isom R , S ( A , B ) /\ A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) ) /\ ( d e. A /\ e e. A /\ f e. A ) ) -> ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) )
52 51 ralrimivvva 
 |-  ( ( H Isom R , S ( A , B ) /\ A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) ) -> A. d e. A A. e e. A A. f e. A ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) )
53 52 ex 
 |-  ( H Isom R , S ( A , B ) -> ( A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) -> A. d e. A A. e e. A A. f e. A ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) ) )
54 df-po 
 |-  ( S Po B <-> A. a e. B A. b e. B A. c e. B ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) )
55 df-po 
 |-  ( R Po A <-> A. d e. A A. e e. A A. f e. A ( -. d R d /\ ( ( d R e /\ e R f ) -> d R f ) ) )
56 53 54 55 3imtr4g 
 |-  ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )