Metamath Proof Explorer

Theorem erdsze2lem2

Description: Lemma for erdsze2 . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze2.r 
|- ( ph -> R e. NN )
erdsze2.s 
|- ( ph -> S e. NN )
erdsze2.f 
|- ( ph -> F : A -1-1-> RR )
erdsze2.a 
|- ( ph -> A C_ RR )
erdsze2lem.n 
|- N = ( ( R - 1 ) x. ( S - 1 ) )
erdsze2lem.l 
|- ( ph -> N < ( # ` A ) )
erdsze2lem.g 
|- ( ph -> G : ( 1 ... ( N + 1 ) ) -1-1-> A )
erdsze2lem.i 
|- ( ph -> G Isom < , < ( ( 1 ... ( N + 1 ) ) , ran G ) )
Assertion erdsze2lem2 
|- ( ph -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r 
 |-  ( ph -> R e. NN )
2 erdsze2.s 
 |-  ( ph -> S e. NN )
3 erdsze2.f 
 |-  ( ph -> F : A -1-1-> RR )
4 erdsze2.a 
 |-  ( ph -> A C_ RR )
5 erdsze2lem.n 
 |-  N = ( ( R - 1 ) x. ( S - 1 ) )
6 erdsze2lem.l 
 |-  ( ph -> N < ( # ` A ) )
7 erdsze2lem.g 
 |-  ( ph -> G : ( 1 ... ( N + 1 ) ) -1-1-> A )
8 erdsze2lem.i 
 |-  ( ph -> G Isom < , < ( ( 1 ... ( N + 1 ) ) , ran G ) )
9 nnm1nn0 
 |-  ( R e. NN -> ( R - 1 ) e. NN0 )
10 1 9 syl 
 |-  ( ph -> ( R - 1 ) e. NN0 )
11 nnm1nn0 
 |-  ( S e. NN -> ( S - 1 ) e. NN0 )
12 2 11 syl 
 |-  ( ph -> ( S - 1 ) e. NN0 )
13 10 12 nn0mulcld 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) e. NN0 )
14 5 13 eqeltrid 
 |-  ( ph -> N e. NN0 )
15 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
16 14 15 syl 
 |-  ( ph -> ( N + 1 ) e. NN )
17 f1co 
 |-  ( ( F : A -1-1-> RR /\ G : ( 1 ... ( N + 1 ) ) -1-1-> A ) -> ( F o. G ) : ( 1 ... ( N + 1 ) ) -1-1-> RR )
18 3 7 17 syl2anc 
 |-  ( ph -> ( F o. G ) : ( 1 ... ( N + 1 ) ) -1-1-> RR )
19 14 nn0red 
 |-  ( ph -> N e. RR )
20 19 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
21 5 20 eqbrtrrid 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < ( N + 1 ) )
22 16 18 1 2 21 erdsze 
 |-  ( ph -> E. t e. ~P ( 1 ... ( N + 1 ) ) ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) \/ ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) ) )
23 velpw 
 |-  ( t e. ~P ( 1 ... ( N + 1 ) ) <-> t C_ ( 1 ... ( N + 1 ) ) )
24 imassrn 
 |-  ( G " t ) C_ ran G
25 f1f 
 |-  ( G : ( 1 ... ( N + 1 ) ) -1-1-> A -> G : ( 1 ... ( N + 1 ) ) --> A )
26 7 25 syl 
 |-  ( ph -> G : ( 1 ... ( N + 1 ) ) --> A )
27 26 frnd 
 |-  ( ph -> ran G C_ A )
28 24 27 sstrid 
 |-  ( ph -> ( G " t ) C_ A )
29 reex 
 |-  RR e. _V
30 ssexg 
 |-  ( ( A C_ RR /\ RR e. _V ) -> A e. _V )
31 4 29 30 sylancl 
 |-  ( ph -> A e. _V )
32 elpw2g 
 |-  ( A e. _V -> ( ( G " t ) e. ~P A <-> ( G " t ) C_ A ) )
33 31 32 syl 
 |-  ( ph -> ( ( G " t ) e. ~P A <-> ( G " t ) C_ A ) )
34 28 33 mpbird 
 |-  ( ph -> ( G " t ) e. ~P A )
35 34 adantr 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G " t ) e. ~P A )
36 vex 
 |-  t e. _V
37 36 f1imaen 
 |-  ( ( G : ( 1 ... ( N + 1 ) ) -1-1-> A /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G " t ) ~~ t )
38 7 37 sylan 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G " t ) ~~ t )
39 fzfid 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( 1 ... ( N + 1 ) ) e. Fin )
40 simpr 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> t C_ ( 1 ... ( N + 1 ) ) )
41 ssfi 
 |-  ( ( ( 1 ... ( N + 1 ) ) e. Fin /\ t C_ ( 1 ... ( N + 1 ) ) ) -> t e. Fin )
42 39 40 41 syl2anc 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> t e. Fin )
43 enfii 
 |-  ( ( t e. Fin /\ ( G " t ) ~~ t ) -> ( G " t ) e. Fin )
44 42 38 43 syl2anc 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G " t ) e. Fin )
45 hashen 
 |-  ( ( ( G " t ) e. Fin /\ t e. Fin ) -> ( ( # ` ( G " t ) ) = ( # ` t ) <-> ( G " t ) ~~ t ) )
46 44 42 45 syl2anc 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( # ` ( G " t ) ) = ( # ` t ) <-> ( G " t ) ~~ t ) )
47 38 46 mpbird 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( # ` ( G " t ) ) = ( # ` t ) )
48 47 breq2d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( R <_ ( # ` ( G " t ) ) <-> R <_ ( # ` t ) ) )
49 48 biimprd 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( R <_ ( # ` t ) -> R <_ ( # ` ( G " t ) ) ) )
50 8 ad2antrr 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> G Isom < , < ( ( 1 ... ( N + 1 ) ) , ran G ) )
51 40 adantr 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> t C_ ( 1 ... ( N + 1 ) ) )
52 simprl 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> x e. t )
53 51 52 sseldd 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> x e. ( 1 ... ( N + 1 ) ) )
54 simprr 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> y e. t )
55 51 54 sseldd 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> y e. ( 1 ... ( N + 1 ) ) )
56 isorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( N + 1 ) ) , ran G ) /\ ( x e. ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) ) -> ( x < y <-> ( G ` x ) < ( G ` y ) ) )
57 50 53 55 56 syl12anc 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> ( x < y <-> ( G ` x ) < ( G ` y ) ) )
58 57 biimpd 
 |-  ( ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) /\ ( x e. t /\ y e. t ) ) -> ( x < y -> ( G ` x ) < ( G ` y ) ) )
59 58 ralrimivva 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> A. x e. t A. y e. t ( x < y -> ( G ` x ) < ( G ` y ) ) )
60 elfznn 
 |-  ( t e. ( 1 ... ( N + 1 ) ) -> t e. NN )
61 60 nnred 
 |-  ( t e. ( 1 ... ( N + 1 ) ) -> t e. RR )
62 61 ssriv 
 |-  ( 1 ... ( N + 1 ) ) C_ RR
63 62 a1i 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( 1 ... ( N + 1 ) ) C_ RR )
64 ltso 
 |-  < Or RR
65 soss 
 |-  ( ( 1 ... ( N + 1 ) ) C_ RR -> ( < Or RR -> < Or ( 1 ... ( N + 1 ) ) ) )
66 63 64 65 mpisyl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> < Or ( 1 ... ( N + 1 ) ) )
67 4 adantr 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> A C_ RR )
68 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
69 67 64 68 mpisyl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> < Or A )
70 26 adantr 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> G : ( 1 ... ( N + 1 ) ) --> A )
71 soisores 
 |-  ( ( ( < Or ( 1 ... ( N + 1 ) ) /\ < Or A ) /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ t C_ ( 1 ... ( N + 1 ) ) ) ) -> ( ( G |` t ) Isom < , < ( t , ( G " t ) ) <-> A. x e. t A. y e. t ( x < y -> ( G ` x ) < ( G ` y ) ) ) )
72 66 69 70 40 71 syl22anc 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( G |` t ) Isom < , < ( t , ( G " t ) ) <-> A. x e. t A. y e. t ( x < y -> ( G ` x ) < ( G ` y ) ) ) )
73 59 72 mpbird 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G |` t ) Isom < , < ( t , ( G " t ) ) )
74 isocnv 
 |-  ( ( G |` t ) Isom < , < ( t , ( G " t ) ) -> `' ( G |` t ) Isom < , < ( ( G " t ) , t ) )
75 73 74 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> `' ( G |` t ) Isom < , < ( ( G " t ) , t ) )
76 isotr 
 |-  ( ( `' ( G |` t ) Isom < , < ( ( G " t ) , t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) )
77 76 ex 
 |-  ( `' ( G |` t ) Isom < , < ( ( G " t ) , t ) -> ( ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
78 75 77 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
79 resco 
 |-  ( ( F o. G ) |` t ) = ( F o. ( G |` t ) )
80 79 coeq1i 
 |-  ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) = ( ( F o. ( G |` t ) ) o. `' ( G |` t ) )
81 coass 
 |-  ( ( F o. ( G |` t ) ) o. `' ( G |` t ) ) = ( F o. ( ( G |` t ) o. `' ( G |` t ) ) )
82 80 81 eqtri 
 |-  ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) = ( F o. ( ( G |` t ) o. `' ( G |` t ) ) )
83 f1ores 
 |-  ( ( G : ( 1 ... ( N + 1 ) ) -1-1-> A /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G |` t ) : t -1-1-onto-> ( G " t ) )
84 7 83 sylan 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( G |` t ) : t -1-1-onto-> ( G " t ) )
85 f1ococnv2 
 |-  ( ( G |` t ) : t -1-1-onto-> ( G " t ) -> ( ( G |` t ) o. `' ( G |` t ) ) = ( _I |` ( G " t ) ) )
86 84 85 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( G |` t ) o. `' ( G |` t ) ) = ( _I |` ( G " t ) ) )
87 86 coeq2d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( F o. ( ( G |` t ) o. `' ( G |` t ) ) ) = ( F o. ( _I |` ( G " t ) ) ) )
88 coires1 
 |-  ( F o. ( _I |` ( G " t ) ) ) = ( F |` ( G " t ) )
89 87 88 eqtrdi 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( F o. ( ( G |` t ) o. `' ( G |` t ) ) ) = ( F |` ( G " t ) ) )
90 82 89 syl5eq 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) = ( F |` ( G " t ) ) )
91 isoeq1 
 |-  ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) = ( F |` ( G " t ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
92 90 91 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
93 imaco 
 |-  ( ( F o. G ) " t ) = ( F " ( G " t ) )
94 isoeq5 
 |-  ( ( ( F o. G ) " t ) = ( F " ( G " t ) ) -> ( ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
95 93 94 ax-mp 
 |-  ( ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) )
96 92 95 bitrdi 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
97 78 96 sylibd 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) -> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
98 49 97 anim12d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) -> ( R <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) )
99 47 breq2d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( S <_ ( # ` ( G " t ) ) <-> S <_ ( # ` t ) ) )
100 99 biimprd 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( S <_ ( # ` t ) -> S <_ ( # ` ( G " t ) ) ) )
101 isotr 
 |-  ( ( `' ( G |` t ) Isom < , < ( ( G " t ) , t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) )
102 101 ex 
 |-  ( `' ( G |` t ) Isom < , < ( ( G " t ) , t ) -> ( ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
103 75 102 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) -> ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
104 isoeq1 
 |-  ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) = ( F |` ( G " t ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
105 90 104 syl 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) ) )
106 isoeq5 
 |-  ( ( ( F o. G ) " t ) = ( F " ( G " t ) ) -> ( ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
107 93 106 ax-mp 
 |-  ( ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) )
108 105 107 bitrdi 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( F o. G ) |` t ) o. `' ( G |` t ) ) Isom < , `' < ( ( G " t ) , ( ( F o. G ) " t ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
109 103 108 sylibd 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) -> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
110 100 109 anim12d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) -> ( S <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) )
111 98 110 orim12d 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) \/ ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) ) -> ( ( R <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) \/ ( S <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) ) )
112 fveq2 
 |-  ( s = ( G " t ) -> ( # ` s ) = ( # ` ( G " t ) ) )
113 112 breq2d 
 |-  ( s = ( G " t ) -> ( R <_ ( # ` s ) <-> R <_ ( # ` ( G " t ) ) ) )
114 reseq2 
 |-  ( s = ( G " t ) -> ( F |` s ) = ( F |` ( G " t ) ) )
115 isoeq1 
 |-  ( ( F |` s ) = ( F |` ( G " t ) ) -> ( ( F |` s ) Isom < , < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( s , ( F " s ) ) ) )
116 114 115 syl 
 |-  ( s = ( G " t ) -> ( ( F |` s ) Isom < , < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( s , ( F " s ) ) ) )
117 isoeq4 
 |-  ( s = ( G " t ) -> ( ( F |` ( G " t ) ) Isom < , < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " s ) ) ) )
118 imaeq2 
 |-  ( s = ( G " t ) -> ( F " s ) = ( F " ( G " t ) ) )
119 isoeq5 
 |-  ( ( F " s ) = ( F " ( G " t ) ) -> ( ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
120 118 119 syl 
 |-  ( s = ( G " t ) -> ( ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
121 116 117 120 3bitrd 
 |-  ( s = ( G " t ) -> ( ( F |` s ) Isom < , < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
122 113 121 anbi12d 
 |-  ( s = ( G " t ) -> ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) <-> ( R <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) )
123 112 breq2d 
 |-  ( s = ( G " t ) -> ( S <_ ( # ` s ) <-> S <_ ( # ` ( G " t ) ) ) )
124 isoeq1 
 |-  ( ( F |` s ) = ( F |` ( G " t ) ) -> ( ( F |` s ) Isom < , `' < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( s , ( F " s ) ) ) )
125 114 124 syl 
 |-  ( s = ( G " t ) -> ( ( F |` s ) Isom < , `' < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( s , ( F " s ) ) ) )
126 isoeq4 
 |-  ( s = ( G " t ) -> ( ( F |` ( G " t ) ) Isom < , `' < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " s ) ) ) )
127 isoeq5 
 |-  ( ( F " s ) = ( F " ( G " t ) ) -> ( ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
128 118 127 syl 
 |-  ( s = ( G " t ) -> ( ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
129 125 126 128 3bitrd 
 |-  ( s = ( G " t ) -> ( ( F |` s ) Isom < , `' < ( s , ( F " s ) ) <-> ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) )
130 123 129 anbi12d 
 |-  ( s = ( G " t ) -> ( ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) <-> ( S <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) )
131 122 130 orbi12d 
 |-  ( s = ( G " t ) -> ( ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) <-> ( ( R <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) \/ ( S <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) ) )
132 131 rspcev 
 |-  ( ( ( G " t ) e. ~P A /\ ( ( R <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , < ( ( G " t ) , ( F " ( G " t ) ) ) ) \/ ( S <_ ( # ` ( G " t ) ) /\ ( F |` ( G " t ) ) Isom < , `' < ( ( G " t ) , ( F " ( G " t ) ) ) ) ) ) -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )
133 35 111 132 syl6an 
 |-  ( ( ph /\ t C_ ( 1 ... ( N + 1 ) ) ) -> ( ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) \/ ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) ) -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) )
134 23 133 sylan2b 
 |-  ( ( ph /\ t e. ~P ( 1 ... ( N + 1 ) ) ) -> ( ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) \/ ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) ) -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) )
135 134 rexlimdva 
 |-  ( ph -> ( E. t e. ~P ( 1 ... ( N + 1 ) ) ( ( R <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , < ( t , ( ( F o. G ) " t ) ) ) \/ ( S <_ ( # ` t ) /\ ( ( F o. G ) |` t ) Isom < , `' < ( t , ( ( F o. G ) " t ) ) ) ) -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) )
136 22 135 mpd 
 |-  ( ph -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )