Metamath Proof Explorer

Theorem fourierdlem20

Description: Every interval in the partition S is included in an interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem20.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem20.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem20.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem20.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
fourierdlem20.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
fourierdlem20.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
fourierdlem20.qm ⊢ ( 𝜑 → 𝐵 ≤ ( 𝑄 ‘ 𝑀 ) )
fourierdlem20.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem20.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
fourierdlem20.s ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
fourierdlem20.i ⊢ 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < )
Assertion fourierdlem20 ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem20.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 fourierdlem20.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 fourierdlem20.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 fourierdlem20.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 fourierdlem20.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
6 fourierdlem20.q0 ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
7 fourierdlem20.qm ⊢ ( 𝜑 → 𝐵 ≤ ( 𝑄 ‘ 𝑀 ) )
8 fourierdlem20.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
9 fourierdlem20.t ⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
10 fourierdlem20.s ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
11 fourierdlem20.i ⊢ 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < )
12 ssrab2 ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ( 0 ..^ 𝑀 )
13 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
14 fzssz ⊢ ( 0 ... 𝑀 ) ⊆ ℤ
15 13 14 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℤ
16 12 15 sstri ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℤ
17 16 a1i ⊢ ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℤ )
18 0z ⊢ 0 ∈ ℤ
19 0le0 ⊢ 0 ≤ 0
20 eluz2 ⊢ ( 0 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0 ) )
21 18 18 19 20 mpbir3an ⊢ 0 ∈ ( ℤ≥ ‘ 0 )
22 21 a1i ⊢ ( 𝜑 → 0 ∈ ( ℤ≥ ‘ 0 ) )
23 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
24 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
25 elfzo2 ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
26 22 23 24 25 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
27 13 26 sselid ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
28 5 27 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
29 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
30 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
31 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
32 29 30 4 31 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
33 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
34 29 30 4 33 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
35 32 34 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) )
36 prssg ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
37 29 30 36 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
38 35 37 mpbid ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) )
39 inss2 ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 )
40 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
41 39 40 sstri ⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 )
42 41 a1i ⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
43 38 42 unssd ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
44 9 43 eqsstrid ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
45 2 3 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
46 44 45 sstrd ⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
47 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
48 f1of ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
49 10 47 48 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
50 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
51 8 50 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
52 49 51 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ 𝑇 )
53 46 52 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
54 44 52 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐴 [,] 𝐵 ) )
55 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑆 ‘ 𝐽 ) )
56 29 30 54 55 syl3anc ⊢ ( 𝜑 → 𝐴 ≤ ( 𝑆 ‘ 𝐽 ) )
57 28 2 53 6 56 letrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ ( 𝑆 ‘ 𝐽 ) )
58 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 0 ) )
59 58 breq1d ⊢ ( 𝑘 = 0 → ( ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) ↔ ( 𝑄 ‘ 0 ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
60 59 elrab ⊢ ( 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
61 26 57 60 sylanbrc ⊢ ( 𝜑 → 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } )
62 61 ne0d ⊢ ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ≠ ∅ )
63 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
64 12 sseli ⊢ ( 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
65 elfzo0le ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ≤ 𝑀 )
66 64 65 syl ⊢ ( 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } → 𝑗 ≤ 𝑀 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ) → 𝑗 ≤ 𝑀 )
68 67 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑀 )
69 breq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀 ) )
70 69 ralbidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 ↔ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑀 ) )
71 70 rspcev ⊢ ( ( 𝑀 ∈ ℝ ∧ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑀 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 )
72 63 68 71 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 )
73 suprzcl ⊢ ( ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℤ ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 ) → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } )
74 17 62 72 73 syl3anc ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } )
75 12 74 sselid ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
76 11 75 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
77 13 76 sselid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
78 5 77 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
79 78 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
80 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
81 76 80 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
82 5 81 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
83 82 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
84 11 74 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } )
85 nfrab1 ⊢ Ⅎ 𝑘 { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) }
86 nfcv ⊢ Ⅎ 𝑘 ℝ
87 nfcv ⊢ Ⅎ 𝑘 <
88 85 86 87 nfsup ⊢ Ⅎ 𝑘 sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < )
89 11 88 nfcxfr ⊢ Ⅎ 𝑘 𝐼
90 nfcv ⊢ Ⅎ 𝑘 ( 0 ..^ 𝑀 )
91 nfcv ⊢ Ⅎ 𝑘 𝑄
92 91 89 nffv ⊢ Ⅎ 𝑘 ( 𝑄 ‘ 𝐼 )
93 nfcv ⊢ Ⅎ 𝑘 ≤
94 nfcv ⊢ Ⅎ 𝑘 ( 𝑆 ‘ 𝐽 )
95 92 93 94 nfbr ⊢ Ⅎ 𝑘 ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 )
96 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝐼 ) )
97 96 breq1d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) ↔ ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
98 89 90 95 97 elrabf ⊢ ( 𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ↔ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
99 84 98 sylib ⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
100 99 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 ) )
101 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
102 83 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
103 iccssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
104 44 103 sstrdi ⊢ ( 𝜑 → 𝑇 ⊆ ℝ* )
105 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
106 8 105 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
107 49 106 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ 𝑇 )
108 104 107 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
109 108 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
110 xrltnle ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
111 102 109 110 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
112 101 111 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
113 fzssz ⊢ ( 0 ... 𝑁 ) ⊆ ℤ
114 f1ofo ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 )
115 10 47 114 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 )
116 115 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 )
117 ffun ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → Fun 𝑄 )
118 5 117 syl ⊢ ( 𝜑 → Fun 𝑄 )
119 5 fdmd ⊢ ( 𝜑 → dom 𝑄 = ( 0 ... 𝑀 ) )
120 119 eqcomd ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = dom 𝑄 )
121 81 120 eleqtrd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ dom 𝑄 )
122 fvelrn ⊢ ( ( Fun 𝑄 ∧ ( 𝐼 + 1 ) ∈ dom 𝑄 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
123 118 121 122 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
124 123 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
125 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐴 ∈ ℝ* )
126 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐵 ∈ ℝ* )
127 82 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
128 45 54 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
129 14 sseli ⊢ ( 𝐼 ∈ ( 0 ... 𝑀 ) → 𝐼 ∈ ℤ )
130 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
131 77 129 130 3syl ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
132 131 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 ∈ ℝ )
133 132 ltp1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 < ( 𝐼 + 1 ) )
134 133 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 < ( 𝐼 + 1 ) )
135 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
136 128 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
137 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
138 135 136 137 nltled ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) )
139 131 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → 𝐼 ∈ ℝ )
140 1red ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → 1 ∈ ℝ )
141 139 140 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
142 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℤ )
143 142 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
144 143 ssriv ⊢ ( 0 ..^ 𝑀 ) ⊆ ℝ
145 12 144 sstri ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℝ
146 145 a1i ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℝ )
147 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ≠ ∅ )
148 72 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 )
149 82 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
150 128 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
151 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → 𝐵 ∈ ℝ )
152 simpr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) )
153 46 107 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
154 153 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
155 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
156 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
157 8 155 156 3syl ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
158 157 ltp1d ⊢ ( 𝜑 → 𝐽 < ( 𝐽 + 1 ) )
159 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
160 10 51 106 159 syl12anc ⊢ ( 𝜑 → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
161 158 160 mpbid ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
162 161 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
163 44 107 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
164 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
165 29 30 163 164 syl3anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
166 165 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
167 150 154 151 162 166 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑆 ‘ 𝐽 ) < 𝐵 )
168 149 150 151 152 167 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
169 168 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
170 3 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ ℝ )
171 82 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
172 7 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ≤ ( 𝑄 ‘ 𝑀 ) )
173 23 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℤ )
174 81 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
175 fzval3 ⊢ ( 𝑀 ∈ ℤ → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
176 23 175 syl ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
177 176 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
178 174 177 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) )
179 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
180 178 179 jca ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
181 elfzonelfzo ⊢ ( 𝑀 ∈ ℤ → ( ( ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ) )
182 173 180 181 sylc ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
183 fzval3 ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
184 23 183 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
185 184 eqcomd ⊢ ( 𝜑 → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = ( 𝑀 ... 𝑀 ) )
186 185 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = ( 𝑀 ... 𝑀 ) )
187 182 186 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑀 ) )
188 elfz1eq ⊢ ( ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑀 ) → ( 𝐼 + 1 ) = 𝑀 )
189 187 188 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) = 𝑀 )
190 189 eqcomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 = ( 𝐼 + 1 ) )
191 190 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
192 172 191 breqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
193 170 171 192 lensymd ⊢ ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
194 193 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
195 169 194 condan ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
196 nfcv ⊢ Ⅎ 𝑘 +
197 nfcv ⊢ Ⅎ 𝑘 1
198 89 196 197 nfov ⊢ Ⅎ 𝑘 ( 𝐼 + 1 )
199 91 198 nffv ⊢ Ⅎ 𝑘 ( 𝑄 ‘ ( 𝐼 + 1 ) )
200 199 93 94 nfbr ⊢ Ⅎ 𝑘 ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 )
201 fveq2 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
202 201 breq1d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
203 198 90 200 202 elrabf ⊢ ( ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) )
204 195 152 203 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } )
205 suprub ⊢ ( ( ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ⊆ ℝ ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } 𝑗 ≤ 𝑥 ) ∧ ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) )
206 146 147 148 204 205 syl31anc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) ≤ ( 𝑆 ‘ 𝐽 ) } , ℝ , < ) )
207 206 11 breqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐼 + 1 ) ≤ 𝐼 )
208 141 139 207 lensymd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
209 208 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆 ‘ 𝐽 ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
210 138 209 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
211 134 210 condan ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
212 82 211 mpdan ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
213 2 128 82 56 212 lelttrd ⊢ ( 𝜑 → 𝐴 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
214 213 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐴 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
215 153 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
216 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐵 ∈ ℝ )
217 simpr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
218 165 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
219 127 215 216 217 218 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
220 125 126 127 214 219 eliood ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 (,) 𝐵 ) )
221 124 220 elind ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
222 elun2 ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) )
223 221 222 syl ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) )
224 223 9 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 )
225 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) )
226 116 224 225 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) )
227 212 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
228 simpr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) )
229 227 228 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) )
230 229 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) )
231 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
232 51 anim1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) )
233 232 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) )
234 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) )
235 231 233 234 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) )
236 230 235 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → 𝐽 < 𝑗 )
237 236 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → 𝐽 < 𝑗 )
238 eqcom ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ↔ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
239 238 biimpi ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) → ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
240 239 adantl ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
241 simpl ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
242 240 241 eqbrtrd ⊢ ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
243 242 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
244 243 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
245 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
246 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
247 106 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
248 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
249 245 246 247 248 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
250 249 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
251 244 250 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → 𝑗 < ( 𝐽 + 1 ) )
252 237 251 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) ) → ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
253 252 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) → ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
254 253 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆 ‘ 𝑗 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
255 226 254 mpd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
256 ssrexv ⊢ ( ( 0 ... 𝑁 ) ⊆ ℤ → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) )
257 113 255 256 mpsyl ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
258 112 257 syldan ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
259 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 ∈ ℤ )
260 8 155 syl ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
261 260 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 ∈ ℤ )
262 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 < 𝑗 )
263 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
264 btwnnz ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) → ¬ 𝑗 ∈ ℤ )
265 261 262 263 264 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) ) → ¬ 𝑗 ∈ ℤ )
266 259 265 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ¬ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
267 266 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
268 267 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) )
269 258 268 condan ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
270 ioossioo ⊢ ( ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑄 ‘ 𝐼 ) ≤ ( 𝑆 ‘ 𝐽 ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
271 79 83 100 269 270 syl22anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
272 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝐼 ) )
273 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 + 1 ) = ( 𝐼 + 1 ) )
274 273 fveq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
275 272 274 oveq12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
276 275 sseq2d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
277 276 rspcev ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
278 76 271 277 syl2anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )