Metamath Proof Explorer

Theorem supisolem

Description: Lemma for supiso . (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 
|- ( ph -> F Isom R , S ( A , B ) )
supiso.2 
|- ( ph -> C C_ A )
Assertion supisolem 
|- ( ( ph /\ D e. A ) -> ( ( A. y e. C -. D R y /\ A. y e. A ( y R D -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` D ) S w /\ A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) ) )

Proof

Step Hyp Ref Expression
1 supiso.1 
 |-  ( ph -> F Isom R , S ( A , B ) )
2 supiso.2 
 |-  ( ph -> C C_ A )
3 1 2 jca 
 |-  ( ph -> ( F Isom R , S ( A , B ) /\ C C_ A ) )
4 simpll 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> F Isom R , S ( A , B ) )
5 4 adantr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. C ) -> F Isom R , S ( A , B ) )
6 simplr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. C ) -> D e. A )
7 simplr 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> C C_ A )
8 7 sselda 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. C ) -> y e. A )
9 isorel 
 |-  ( ( F Isom R , S ( A , B ) /\ ( D e. A /\ y e. A ) ) -> ( D R y <-> ( F ` D ) S ( F ` y ) ) )
10 5 6 8 9 syl12anc 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. C ) -> ( D R y <-> ( F ` D ) S ( F ` y ) ) )
11 10 notbid 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. C ) -> ( -. D R y <-> -. ( F ` D ) S ( F ` y ) ) )
12 11 ralbidva 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. y e. C -. D R y <-> A. y e. C -. ( F ` D ) S ( F ` y ) ) )
13 isof1o 
 |-  ( F Isom R , S ( A , B ) -> F : A -1-1-onto-> B )
14 4 13 syl 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> F : A -1-1-onto-> B )
15 f1ofn 
 |-  ( F : A -1-1-onto-> B -> F Fn A )
16 14 15 syl 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> F Fn A )
17 breq2 
 |-  ( w = ( F ` y ) -> ( ( F ` D ) S w <-> ( F ` D ) S ( F ` y ) ) )
18 17 notbid 
 |-  ( w = ( F ` y ) -> ( -. ( F ` D ) S w <-> -. ( F ` D ) S ( F ` y ) ) )
19 18 ralima 
 |-  ( ( F Fn A /\ C C_ A ) -> ( A. w e. ( F " C ) -. ( F ` D ) S w <-> A. y e. C -. ( F ` D ) S ( F ` y ) ) )
20 16 7 19 syl2anc 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. w e. ( F " C ) -. ( F ` D ) S w <-> A. y e. C -. ( F ` D ) S ( F ` y ) ) )
21 12 20 bitr4d 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. y e. C -. D R y <-> A. w e. ( F " C ) -. ( F ` D ) S w ) )
22 4 adantr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> F Isom R , S ( A , B ) )
23 simpr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> y e. A )
24 simplr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> D e. A )
25 isorel 
 |-  ( ( F Isom R , S ( A , B ) /\ ( y e. A /\ D e. A ) ) -> ( y R D <-> ( F ` y ) S ( F ` D ) ) )
26 22 23 24 25 syl12anc 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> ( y R D <-> ( F ` y ) S ( F ` D ) ) )
27 22 adantr 
 |-  ( ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) /\ z e. C ) -> F Isom R , S ( A , B ) )
28 simplr 
 |-  ( ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) /\ z e. C ) -> y e. A )
29 7 adantr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> C C_ A )
30 29 sselda 
 |-  ( ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) /\ z e. C ) -> z e. A )
31 isorel 
 |-  ( ( F Isom R , S ( A , B ) /\ ( y e. A /\ z e. A ) ) -> ( y R z <-> ( F ` y ) S ( F ` z ) ) )
32 27 28 30 31 syl12anc 
 |-  ( ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) /\ z e. C ) -> ( y R z <-> ( F ` y ) S ( F ` z ) ) )
33 32 rexbidva 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> ( E. z e. C y R z <-> E. z e. C ( F ` y ) S ( F ` z ) ) )
34 16 adantr 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> F Fn A )
35 breq2 
 |-  ( v = ( F ` z ) -> ( ( F ` y ) S v <-> ( F ` y ) S ( F ` z ) ) )
36 35 rexima 
 |-  ( ( F Fn A /\ C C_ A ) -> ( E. v e. ( F " C ) ( F ` y ) S v <-> E. z e. C ( F ` y ) S ( F ` z ) ) )
37 34 29 36 syl2anc 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> ( E. v e. ( F " C ) ( F ` y ) S v <-> E. z e. C ( F ` y ) S ( F ` z ) ) )
38 33 37 bitr4d 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> ( E. z e. C y R z <-> E. v e. ( F " C ) ( F ` y ) S v ) )
39 26 38 imbi12d 
 |-  ( ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) /\ y e. A ) -> ( ( y R D -> E. z e. C y R z ) <-> ( ( F ` y ) S ( F ` D ) -> E. v e. ( F " C ) ( F ` y ) S v ) ) )
40 39 ralbidva 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. y e. A ( y R D -> E. z e. C y R z ) <-> A. y e. A ( ( F ` y ) S ( F ` D ) -> E. v e. ( F " C ) ( F ` y ) S v ) ) )
41 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
42 breq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) S ( F ` D ) <-> w S ( F ` D ) ) )
43 breq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) S v <-> w S v ) )
44 43 rexbidv 
 |-  ( ( F ` y ) = w -> ( E. v e. ( F " C ) ( F ` y ) S v <-> E. v e. ( F " C ) w S v ) )
45 42 44 imbi12d 
 |-  ( ( F ` y ) = w -> ( ( ( F ` y ) S ( F ` D ) -> E. v e. ( F " C ) ( F ` y ) S v ) <-> ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) )
46 45 cbvfo 
 |-  ( F : A -onto-> B -> ( A. y e. A ( ( F ` y ) S ( F ` D ) -> E. v e. ( F " C ) ( F ` y ) S v ) <-> A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) )
47 14 41 46 3syl 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. y e. A ( ( F ` y ) S ( F ` D ) -> E. v e. ( F " C ) ( F ` y ) S v ) <-> A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) )
48 40 47 bitrd 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( A. y e. A ( y R D -> E. z e. C y R z ) <-> A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) )
49 21 48 anbi12d 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ D e. A ) -> ( ( A. y e. C -. D R y /\ A. y e. A ( y R D -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` D ) S w /\ A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) ) )
50 3 49 sylan 
 |-  ( ( ph /\ D e. A ) -> ( ( A. y e. C -. D R y /\ A. y e. A ( y R D -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` D ) S w /\ A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) ) )