Metamath Proof Explorer

Theorem erdsze2lem2

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

Ref Expression
Hypotheses erdsze2.r ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
erdsze2lem.n ⊒ 𝑁 = ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) )
erdsze2lem.l ⊒ ( πœ‘ β†’ 𝑁 < ( β™― β€˜ 𝐴 ) )
erdsze2lem.g ⊒ ( πœ‘ β†’ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
erdsze2lem.i ⊒ ( πœ‘ β†’ 𝐺 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝐺 ) )
Assertion erdsze2lem2 ( πœ‘ β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
2 erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
3 erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
4 erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
5 erdsze2lem.n ⊒ 𝑁 = ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) )
6 erdsze2lem.l ⊒ ( πœ‘ β†’ 𝑁 < ( β™― β€˜ 𝐴 ) )
7 erdsze2lem.g ⊒ ( πœ‘ β†’ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
8 erdsze2lem.i ⊒ ( πœ‘ β†’ 𝐺 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝐺 ) )
9 nnm1nn0 ⊒ ( 𝑅 ∈ β„• β†’ ( 𝑅 βˆ’ 1 ) ∈ β„•0 )
10 1 9 syl ⊒ ( πœ‘ β†’ ( 𝑅 βˆ’ 1 ) ∈ β„•0 )
11 nnm1nn0 ⊒ ( 𝑆 ∈ β„• β†’ ( 𝑆 βˆ’ 1 ) ∈ β„•0 )
12 2 11 syl ⊒ ( πœ‘ β†’ ( 𝑆 βˆ’ 1 ) ∈ β„•0 )
13 10 12 nn0mulcld ⊒ ( πœ‘ β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) ∈ β„•0 )
14 5 13 eqeltrid ⊒ ( πœ‘ β†’ 𝑁 ∈ β„•0 )
15 nn0p1nn ⊒ ( 𝑁 ∈ β„•0 β†’ ( 𝑁 + 1 ) ∈ β„• )
16 14 15 syl ⊒ ( πœ‘ β†’ ( 𝑁 + 1 ) ∈ β„• )
17 f1co ⊒ ( ( 𝐹 : 𝐴 –1-1β†’ ℝ ∧ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ) β†’ ( 𝐹 ∘ 𝐺 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ ℝ )
18 3 7 17 syl2anc ⊒ ( πœ‘ β†’ ( 𝐹 ∘ 𝐺 ) : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ ℝ )
19 14 nn0red ⊒ ( πœ‘ β†’ 𝑁 ∈ ℝ )
20 19 ltp1d ⊒ ( πœ‘ β†’ 𝑁 < ( 𝑁 + 1 ) )
21 5 20 eqbrtrrid ⊒ ( πœ‘ β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) < ( 𝑁 + 1 ) )
22 16 18 1 2 21 erdsze ⊒ ( πœ‘ β†’ βˆƒ 𝑑 ∈ 𝒫 ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ) )
23 velpw ⊒ ( 𝑑 ∈ 𝒫 ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) )
24 imassrn ⊒ ( 𝐺 β€œ 𝑑 ) βŠ† ran 𝐺
25 f1f ⊒ ( 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 β†’ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) ⟢ 𝐴 )
26 7 25 syl ⊒ ( πœ‘ β†’ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) ⟢ 𝐴 )
27 26 frnd ⊒ ( πœ‘ β†’ ran 𝐺 βŠ† 𝐴 )
28 24 27 sstrid ⊒ ( πœ‘ β†’ ( 𝐺 β€œ 𝑑 ) βŠ† 𝐴 )
29 reex ⊒ ℝ ∈ V
30 ssexg ⊒ ( ( 𝐴 βŠ† ℝ ∧ ℝ ∈ V ) β†’ 𝐴 ∈ V )
31 4 29 30 sylancl ⊒ ( πœ‘ β†’ 𝐴 ∈ V )
32 elpw2g ⊒ ( 𝐴 ∈ V β†’ ( ( 𝐺 β€œ 𝑑 ) ∈ 𝒫 𝐴 ↔ ( 𝐺 β€œ 𝑑 ) βŠ† 𝐴 ) )
33 31 32 syl ⊒ ( πœ‘ β†’ ( ( 𝐺 β€œ 𝑑 ) ∈ 𝒫 𝐴 ↔ ( 𝐺 β€œ 𝑑 ) βŠ† 𝐴 ) )
34 28 33 mpbird ⊒ ( πœ‘ β†’ ( 𝐺 β€œ 𝑑 ) ∈ 𝒫 𝐴 )
35 34 adantr ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β€œ 𝑑 ) ∈ 𝒫 𝐴 )
36 vex ⊒ 𝑑 ∈ V
37 36 f1imaen ⊒ ( ( 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β€œ 𝑑 ) β‰ˆ 𝑑 )
38 7 37 sylan ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β€œ 𝑑 ) β‰ˆ 𝑑 )
39 fzfid ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
40 simpr ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) )
41 ssfi ⊒ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ 𝑑 ∈ Fin )
42 39 40 41 syl2anc ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ 𝑑 ∈ Fin )
43 enfii ⊒ ( ( 𝑑 ∈ Fin ∧ ( 𝐺 β€œ 𝑑 ) β‰ˆ 𝑑 ) β†’ ( 𝐺 β€œ 𝑑 ) ∈ Fin )
44 42 38 43 syl2anc ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β€œ 𝑑 ) ∈ Fin )
45 hashen ⊒ ( ( ( 𝐺 β€œ 𝑑 ) ∈ Fin ∧ 𝑑 ∈ Fin ) β†’ ( ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) = ( β™― β€˜ 𝑑 ) ↔ ( 𝐺 β€œ 𝑑 ) β‰ˆ 𝑑 ) )
46 44 42 45 syl2anc ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) = ( β™― β€˜ 𝑑 ) ↔ ( 𝐺 β€œ 𝑑 ) β‰ˆ 𝑑 ) )
47 38 46 mpbird ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) = ( β™― β€˜ 𝑑 ) )
48 47 breq2d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ↔ 𝑅 ≀ ( β™― β€˜ 𝑑 ) ) )
49 48 biimprd ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) β†’ 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ) )
50 8 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ 𝐺 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝐺 ) )
51 40 adantr ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) )
52 simprl ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ π‘₯ ∈ 𝑑 )
53 51 52 sseldd ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ π‘₯ ∈ ( 1 ... ( 𝑁 + 1 ) ) )
54 simprr ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ 𝑦 ∈ 𝑑 )
55 51 54 sseldd ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
56 isorel ⊒ ( ( 𝐺 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝐺 ) ∧ ( π‘₯ ∈ ( 1 ... ( 𝑁 + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) ) β†’ ( π‘₯ < 𝑦 ↔ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) )
57 50 53 55 56 syl12anc ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ ( π‘₯ < 𝑦 ↔ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) )
58 57 biimpd ⊒ ( ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( π‘₯ ∈ 𝑑 ∧ 𝑦 ∈ 𝑑 ) ) β†’ ( π‘₯ < 𝑦 β†’ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) )
59 58 ralrimivva ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ βˆ€ π‘₯ ∈ 𝑑 βˆ€ 𝑦 ∈ 𝑑 ( π‘₯ < 𝑦 β†’ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) )
60 elfznn ⊒ ( 𝑑 ∈ ( 1 ... ( 𝑁 + 1 ) ) β†’ 𝑑 ∈ β„• )
61 60 nnred ⊒ ( 𝑑 ∈ ( 1 ... ( 𝑁 + 1 ) ) β†’ 𝑑 ∈ ℝ )
62 61 ssriv ⊒ ( 1 ... ( 𝑁 + 1 ) ) βŠ† ℝ
63 62 a1i ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 1 ... ( 𝑁 + 1 ) ) βŠ† ℝ )
64 ltso ⊒ < Or ℝ
65 soss ⊒ ( ( 1 ... ( 𝑁 + 1 ) ) βŠ† ℝ β†’ ( < Or ℝ β†’ < Or ( 1 ... ( 𝑁 + 1 ) ) ) )
66 63 64 65 mpisyl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ < Or ( 1 ... ( 𝑁 + 1 ) ) )
67 4 adantr ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ 𝐴 βŠ† ℝ )
68 soss ⊒ ( 𝐴 βŠ† ℝ β†’ ( < Or ℝ β†’ < Or 𝐴 ) )
69 67 64 68 mpisyl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ < Or 𝐴 )
70 26 adantr ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) ⟢ 𝐴 )
71 soisores ⊒ ( ( ( < Or ( 1 ... ( 𝑁 + 1 ) ) ∧ < Or 𝐴 ) ∧ ( 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) ⟢ 𝐴 ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) ) β†’ ( ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( 𝐺 β€œ 𝑑 ) ) ↔ βˆ€ π‘₯ ∈ 𝑑 βˆ€ 𝑦 ∈ 𝑑 ( π‘₯ < 𝑦 β†’ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) ) )
72 66 69 70 40 71 syl22anc ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( 𝐺 β€œ 𝑑 ) ) ↔ βˆ€ π‘₯ ∈ 𝑑 βˆ€ 𝑦 ∈ 𝑑 ( π‘₯ < 𝑦 β†’ ( 𝐺 β€˜ π‘₯ ) < ( 𝐺 β€˜ 𝑦 ) ) ) )
73 59 72 mpbird ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( 𝐺 β€œ 𝑑 ) ) )
74 isocnv ⊒ ( ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( 𝐺 β€œ 𝑑 ) ) β†’ β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) )
75 73 74 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) )
76 isotr ⊒ ( ( β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) )
77 76 ex ⊒ ( β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
78 75 77 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
79 resco ⊒ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) = ( 𝐹 ∘ ( 𝐺 β†Ύ 𝑑 ) )
80 79 coeq1i ⊒ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( ( 𝐹 ∘ ( 𝐺 β†Ύ 𝑑 ) ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) )
81 coass ⊒ ( ( 𝐹 ∘ ( 𝐺 β†Ύ 𝑑 ) ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( 𝐹 ∘ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) )
82 80 81 eqtri ⊒ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( 𝐹 ∘ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) )
83 f1ores ⊒ ( ( 𝐺 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β†Ύ 𝑑 ) : 𝑑 –1-1-ontoβ†’ ( 𝐺 β€œ 𝑑 ) )
84 7 83 sylan ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐺 β†Ύ 𝑑 ) : 𝑑 –1-1-ontoβ†’ ( 𝐺 β€œ 𝑑 ) )
85 f1ococnv2 ⊒ ( ( 𝐺 β†Ύ 𝑑 ) : 𝑑 –1-1-ontoβ†’ ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( I β†Ύ ( 𝐺 β€œ 𝑑 ) ) )
86 84 85 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( I β†Ύ ( 𝐺 β€œ 𝑑 ) ) )
87 86 coeq2d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐹 ∘ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) ) = ( 𝐹 ∘ ( I β†Ύ ( 𝐺 β€œ 𝑑 ) ) ) )
88 coires1 ⊒ ( 𝐹 ∘ ( I β†Ύ ( 𝐺 β€œ 𝑑 ) ) ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) )
89 87 88 eqtrdi ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝐹 ∘ ( ( 𝐺 β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) )
90 82 89 eqtrid ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) )
91 isoeq1 ⊒ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
92 90 91 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
93 imaco ⊒ ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) )
94 isoeq5 ⊒ ( ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
95 93 94 ax-mp ⊒ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) )
96 92 95 bitrdi ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
97 78 96 sylibd ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
98 49 97 anim12d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) β†’ ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) )
99 47 breq2d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ↔ 𝑆 ≀ ( β™― β€˜ 𝑑 ) ) )
100 99 biimprd ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) β†’ 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ) )
101 isotr ⊒ ( ( β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) )
102 101 ex ⊒ ( β—‘ ( 𝐺 β†Ύ 𝑑 ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , 𝑑 ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
103 75 102 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
104 isoeq1 ⊒ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
105 90 104 syl ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) )
106 isoeq5 ⊒ ( ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
107 93 106 ax-mp ⊒ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) )
108 105 107 bitrdi ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) ∘ β—‘ ( 𝐺 β†Ύ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
109 103 108 sylibd ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) β†’ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
110 100 109 anim12d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) β†’ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) )
111 98 110 orim12d ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ) β†’ ( ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) ) )
112 fveq2 ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( β™― β€˜ 𝑠 ) = ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) )
113 112 breq2d ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ↔ 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ) )
114 reseq2 ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( 𝐹 β†Ύ 𝑠 ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) )
115 isoeq1 ⊒ ( ( 𝐹 β†Ύ 𝑠 ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) )
116 114 115 syl ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) )
117 isoeq4 ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ) )
118 imaeq2 ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( 𝐹 β€œ 𝑠 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) )
119 isoeq5 ⊒ ( ( 𝐹 β€œ 𝑠 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
120 118 119 syl ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
121 116 117 120 3bitrd ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
122 113 121 anbi12d ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ↔ ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) )
123 112 breq2d ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ↔ 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ) )
124 isoeq1 ⊒ ( ( 𝐹 β†Ύ 𝑠 ) = ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) )
125 114 124 syl ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) )
126 isoeq4 ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ) )
127 isoeq5 ⊒ ( ( 𝐹 β€œ 𝑠 ) = ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
128 118 127 syl ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
129 125 126 128 3bitrd ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ↔ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) )
130 123 129 anbi12d ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ↔ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) )
131 122 130 orbi12d ⊒ ( 𝑠 = ( 𝐺 β€œ 𝑑 ) β†’ ( ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) ↔ ( ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) ) )
132 131 rspcev ⊒ ( ( ( 𝐺 β€œ 𝑑 ) ∈ 𝒫 𝐴 ∧ ( ( 𝑅 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ ( 𝐺 β€œ 𝑑 ) ) ∧ ( 𝐹 β†Ύ ( 𝐺 β€œ 𝑑 ) ) Isom < , β—‘ < ( ( 𝐺 β€œ 𝑑 ) , ( 𝐹 β€œ ( 𝐺 β€œ 𝑑 ) ) ) ) ) ) β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )
133 35 111 132 syl6an ⊒ ( ( πœ‘ ∧ 𝑑 βŠ† ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ) β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) ) )
134 23 133 sylan2b ⊒ ( ( πœ‘ ∧ 𝑑 ∈ 𝒫 ( 1 ... ( 𝑁 + 1 ) ) ) β†’ ( ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ) β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) ) )
135 134 rexlimdva ⊒ ( πœ‘ β†’ ( βˆƒ 𝑑 ∈ 𝒫 ( 1 ... ( 𝑁 + 1 ) ) ( ( 𝑅 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑑 ) ∧ ( ( 𝐹 ∘ 𝐺 ) β†Ύ 𝑑 ) Isom < , β—‘ < ( 𝑑 , ( ( 𝐹 ∘ 𝐺 ) β€œ 𝑑 ) ) ) ) β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) ) )
136 22 135 mpd ⊒ ( πœ‘ β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )