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 < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )