Metamath Proof Explorer

Theorem isosolem

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

Ref Expression
Assertion isosolem 
|- ( H Isom R , S ( A , B ) -> ( S Or B -> R Or A ) )

Proof

Step Hyp Ref Expression
1 isopolem 
 |-  ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )
2 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
3 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
4 ffvelrn 
 |-  ( ( H : A --> B /\ c e. A ) -> ( H ` c ) e. B )
5 4 ex 
 |-  ( H : A --> B -> ( c e. A -> ( H ` c ) e. B ) )
6 ffvelrn 
 |-  ( ( H : A --> B /\ d e. A ) -> ( H ` d ) e. B )
7 6 ex 
 |-  ( H : A --> B -> ( d e. A -> ( H ` d ) e. B ) )
8 5 7 anim12d 
 |-  ( H : A --> B -> ( ( c e. A /\ d e. A ) -> ( ( H ` c ) e. B /\ ( H ` d ) e. B ) ) )
9 2 3 8 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( ( c e. A /\ d e. A ) -> ( ( H ` c ) e. B /\ ( H ` d ) e. B ) ) )
10 9 imp 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( ( H ` c ) e. B /\ ( H ` d ) e. B ) )
11 breq1 
 |-  ( a = ( H ` c ) -> ( a S b <-> ( H ` c ) S b ) )
12 eqeq1 
 |-  ( a = ( H ` c ) -> ( a = b <-> ( H ` c ) = b ) )
13 breq2 
 |-  ( a = ( H ` c ) -> ( b S a <-> b S ( H ` c ) ) )
14 11 12 13 3orbi123d 
 |-  ( a = ( H ` c ) -> ( ( a S b \/ a = b \/ b S a ) <-> ( ( H ` c ) S b \/ ( H ` c ) = b \/ b S ( H ` c ) ) ) )
15 breq2 
 |-  ( b = ( H ` d ) -> ( ( H ` c ) S b <-> ( H ` c ) S ( H ` d ) ) )
16 eqeq2 
 |-  ( b = ( H ` d ) -> ( ( H ` c ) = b <-> ( H ` c ) = ( H ` d ) ) )
17 breq1 
 |-  ( b = ( H ` d ) -> ( b S ( H ` c ) <-> ( H ` d ) S ( H ` c ) ) )
18 15 16 17 3orbi123d 
 |-  ( b = ( H ` d ) -> ( ( ( H ` c ) S b \/ ( H ` c ) = b \/ b S ( H ` c ) ) <-> ( ( H ` c ) S ( H ` d ) \/ ( H ` c ) = ( H ` d ) \/ ( H ` d ) S ( H ` c ) ) ) )
19 14 18 rspc2v 
 |-  ( ( ( H ` c ) e. B /\ ( H ` d ) e. B ) -> ( A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) -> ( ( H ` c ) S ( H ` d ) \/ ( H ` c ) = ( H ` d ) \/ ( H ` d ) S ( H ` c ) ) ) )
20 10 19 syl 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) -> ( ( H ` c ) S ( H ` d ) \/ ( H ` c ) = ( H ` d ) \/ ( H ` d ) S ( H ` c ) ) ) )
21 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( c R d <-> ( H ` c ) S ( H ` d ) ) )
22 f1of1 
 |-  ( H : A -1-1-onto-> B -> H : A -1-1-> B )
23 2 22 syl 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-> B )
24 f1fveq 
 |-  ( ( H : A -1-1-> B /\ ( c e. A /\ d e. A ) ) -> ( ( H ` c ) = ( H ` d ) <-> c = d ) )
25 23 24 sylan 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( ( H ` c ) = ( H ` d ) <-> c = d ) )
26 25 bicomd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( c = d <-> ( H ` c ) = ( H ` d ) ) )
27 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( d e. A /\ c e. A ) ) -> ( d R c <-> ( H ` d ) S ( H ` c ) ) )
28 27 ancom2s 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( d R c <-> ( H ` d ) S ( H ` c ) ) )
29 21 26 28 3orbi123d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( ( c R d \/ c = d \/ d R c ) <-> ( ( H ` c ) S ( H ` d ) \/ ( H ` c ) = ( H ` d ) \/ ( H ` d ) S ( H ` c ) ) ) )
30 20 29 sylibrd 
 |-  ( ( H Isom R , S ( A , B ) /\ ( c e. A /\ d e. A ) ) -> ( A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) -> ( c R d \/ c = d \/ d R c ) ) )
31 30 ralrimdvva 
 |-  ( H Isom R , S ( A , B ) -> ( A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) -> A. c e. A A. d e. A ( c R d \/ c = d \/ d R c ) ) )
32 1 31 anim12d 
 |-  ( H Isom R , S ( A , B ) -> ( ( S Po B /\ A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) ) -> ( R Po A /\ A. c e. A A. d e. A ( c R d \/ c = d \/ d R c ) ) ) )
33 df-so 
 |-  ( S Or B <-> ( S Po B /\ A. a e. B A. b e. B ( a S b \/ a = b \/ b S a ) ) )
34 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. c e. A A. d e. A ( c R d \/ c = d \/ d R c ) ) )
35 32 33 34 3imtr4g 
 |-  ( H Isom R , S ( A , B ) -> ( S Or B -> R Or A ) )