This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolicc2lem3

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
ovolicc2.10 ⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
ovolicc2.11 ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ 𝑇 )
ovolicc2.12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
ovolicc2.13 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
ovolicc2.14 ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
ovolicc2.15 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
Assertion ovolicc2lem3 ( ( 𝜑 ∧ ( 𝑁 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑃 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ( 𝑁 = 𝑃 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑃 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6 ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7 ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8 ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9 ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10 ovolicc2.10 ⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
11 ovolicc2.11 ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ 𝑇 )
12 ovolicc2.12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
13 ovolicc2.13 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
14 ovolicc2.14 ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
15 ovolicc2.15 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
16 ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
17 2fveq3 ⊢ ( 𝑦 = 𝑘 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) )
18 17 fveq2d ⊢ ( 𝑦 = 𝑘 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) )
19 18 fveq2d ⊢ ( 𝑦 = 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) )
20 2fveq3 ⊢ ( 𝑦 = 𝑁 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) )
21 20 fveq2d ⊢ ( 𝑦 = 𝑁 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) )
22 21 fveq2d ⊢ ( 𝑦 = 𝑁 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) )
23 2fveq3 ⊢ ( 𝑦 = 𝑃 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑃 ) ) )
24 23 fveq2d ⊢ ( 𝑦 = 𝑃 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑃 ) ) ) )
25 24 fveq2d ⊢ ( 𝑦 = 𝑃 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑃 ) ) ) ) )
26 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ⊆ ℕ
27 nnssre ⊢ ℕ ⊆ ℝ
28 26 27 sstri ⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ⊆ ℝ
29 26 sseli ⊢ ( 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } → 𝑦 ∈ ℕ )
30 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
31 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
32 5 30 31 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
34 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝐺 : 𝑈 ⟶ ℕ )
35 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
36 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
37 35 15 36 14 11 algrf ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ 𝑇 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝐾 : ℕ ⟶ 𝑇 )
39 10 ssrab3 ⊢ 𝑇 ⊆ 𝑈
40 fss ⊢ ( ( 𝐾 : ℕ ⟶ 𝑇 ∧ 𝑇 ⊆ 𝑈 ) → 𝐾 : ℕ ⟶ 𝑈 )
41 38 39 40 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝐾 : ℕ ⟶ 𝑈 )
42 ffvelcdm ⊢ ( ( 𝐾 : ℕ ⟶ 𝑈 ∧ 𝑦 ∈ ℕ ) → ( 𝐾 ‘ 𝑦 ) ∈ 𝑈 )
43 41 42 sylancom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝐾 ‘ 𝑦 ) ∈ 𝑈 )
44 34 43 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ∈ ℕ )
45 33 44 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ∈ ( ℝ × ℝ ) )
46 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) ∈ ℝ )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) ∈ ℝ )
48 29 47 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) ∈ ℝ )
49 26 sseli ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } → 𝑘 ∈ ℕ )
50 49 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → 𝑘 ∈ ℕ )
51 29 anim2i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) → ( 𝜑 ∧ 𝑦 ∈ ℕ ) )
52 51 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ( 𝜑 ∧ 𝑦 ∈ ℕ ) )
53 breq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚 ) )
54 53 ralbidv ⊢ ( 𝑛 = 𝑘 → ( ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 ) )
55 54 elrab ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ↔ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 ) )
56 55 simprbi ⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } → ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 )
57 56 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 )
58 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ≤ 𝑚 ↔ 1 ≤ 𝑚 ) )
59 58 ralbidv ⊢ ( 𝑥 = 1 → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀ 𝑚 ∈ 𝑊 1 ≤ 𝑚 ) )
60 breq2 ⊢ ( 𝑥 = 1 → ( 𝑦 < 𝑥 ↔ 𝑦 < 1 ) )
61 2fveq3 ⊢ ( 𝑥 = 1 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) )
62 61 fveq2d ⊢ ( 𝑥 = 1 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) )
63 62 fveq2d ⊢ ( 𝑥 = 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) )
64 63 breq2d ⊢ ( 𝑥 = 1 → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) )
65 60 64 imbi12d ⊢ ( 𝑥 = 1 → ( ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ↔ ( 𝑦 < 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) ) )
66 59 65 imbi12d ⊢ ( 𝑥 = 1 → ( ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ↔ ( ∀ 𝑚 ∈ 𝑊 1 ≤ 𝑚 → ( 𝑦 < 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) ) ) )
67 66 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 1 ≤ 𝑚 → ( 𝑦 < 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) ) ) ) )
68 breq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ≤ 𝑚 ↔ 𝑘 ≤ 𝑚 ) )
69 68 ralbidv ⊢ ( 𝑥 = 𝑘 → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 ) )
70 breq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑘 ) )
71 2fveq3 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) )
72 71 fveq2d ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) )
73 72 fveq2d ⊢ ( 𝑥 = 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) )
74 73 breq2d ⊢ ( 𝑥 = 𝑘 → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) )
75 70 74 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ↔ ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) )
76 69 75 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ↔ ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) )
77 76 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) ) )
78 breq1 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑥 ≤ 𝑚 ↔ ( 𝑘 + 1 ) ≤ 𝑚 ) )
79 78 ralbidv ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 ↔ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) )
80 breq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑦 < 𝑥 ↔ 𝑦 < ( 𝑘 + 1 ) ) )
81 2fveq3 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) )
82 81 fveq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) )
83 82 fveq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) )
84 83 breq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
85 80 84 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ↔ ( 𝑦 < ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
86 79 85 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ↔ ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑦 < ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) ) )
87 86 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑥 ≤ 𝑚 → ( 𝑦 < 𝑥 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑥 ) ) ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑦 < ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) ) ) )
88 nnnlt1 ⊢ ( 𝑦 ∈ ℕ → ¬ 𝑦 < 1 )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ¬ 𝑦 < 1 )
90 89 pm2.21d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝑦 < 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) )
91 90 a1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 1 ≤ 𝑚 → ( 𝑦 < 1 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) ) ) )
92 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
93 92 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → 𝑘 ∈ ℝ )
94 93 lep1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → 𝑘 ≤ ( 𝑘 + 1 ) )
95 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
96 93 95 syl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → ( 𝑘 + 1 ) ∈ ℝ )
97 16 ssrab3 ⊢ 𝑊 ⊆ ℕ
98 97 27 sstri ⊢ 𝑊 ⊆ ℝ
99 98 sseli ⊢ ( 𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ )
100 99 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → 𝑚 ∈ ℝ )
101 letr ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝑘 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑚 ) → 𝑘 ≤ 𝑚 ) )
102 93 96 100 101 syl3anc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑘 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑚 ) → 𝑘 ≤ 𝑚 ) )
103 94 102 mpand ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑊 ) → ( ( 𝑘 + 1 ) ≤ 𝑚 → 𝑘 ≤ 𝑚 ) )
104 103 ralimdva ⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 ) )
105 104 imim1d ⊢ ( 𝑘 ∈ ℕ → ( ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) → ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) )
106 105 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) → ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) )
107 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝑦 ∈ ℕ )
108 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝑘 ∈ ℕ )
109 nnleltp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑦 ≤ 𝑘 ↔ 𝑦 < ( 𝑘 + 1 ) ) )
110 107 108 109 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 ≤ 𝑘 ↔ 𝑦 < ( 𝑘 + 1 ) ) )
111 107 nnred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝑦 ∈ ℝ )
112 108 nnred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝑘 ∈ ℝ )
113 111 112 leloed ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 ≤ 𝑘 ↔ ( 𝑦 < 𝑘 ∨ 𝑦 = 𝑘 ) ) )
114 110 113 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 < ( 𝑘 + 1 ) ↔ ( 𝑦 < 𝑘 ∨ 𝑦 = 𝑘 ) ) )
115 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝜑 )
116 ltp1 ⊢ ( 𝑘 ∈ ℝ → 𝑘 < ( 𝑘 + 1 ) )
117 ltnle ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑘 < ( 𝑘 + 1 ) ↔ ¬ ( 𝑘 + 1 ) ≤ 𝑘 ) )
118 95 117 mpdan ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 < ( 𝑘 + 1 ) ↔ ¬ ( 𝑘 + 1 ) ≤ 𝑘 ) )
119 116 118 mpbid ⊢ ( 𝑘 ∈ ℝ → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
120 112 119 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ¬ ( 𝑘 + 1 ) ≤ 𝑘 )
121 breq2 ⊢ ( 𝑚 = 𝑘 → ( ( 𝑘 + 1 ) ≤ 𝑚 ↔ ( 𝑘 + 1 ) ≤ 𝑘 ) )
122 121 rspccv ⊢ ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑘 ∈ 𝑊 → ( 𝑘 + 1 ) ≤ 𝑘 ) )
123 122 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑘 ∈ 𝑊 → ( 𝑘 + 1 ) ≤ 𝑘 ) )
124 120 123 mtod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ¬ 𝑘 ∈ 𝑊 )
125 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ¬ 𝑘 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 )
126 115 108 124 125 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 )
127 126 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) , 𝐵 ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) )
128 2fveq3 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) )
129 128 fveq2d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) )
130 129 breq1d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 ) )
131 130 129 ifbieq1d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) = if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) , 𝐵 ) )
132 fveq2 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → ( 𝐻 ‘ 𝑡 ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) )
133 131 132 eleq12d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑘 ) → ( if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) ↔ if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) ) )
134 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
135 134 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ∀ 𝑡 ∈ 𝑇 if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
136 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝐾 : ℕ ⟶ 𝑇 )
137 136 108 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐾 ‘ 𝑘 ) ∈ 𝑇 )
138 133 135 137 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) )
139 127 138 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) )
140 35 15 36 14 11 algrp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ‘ ( 𝑘 + 1 ) ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) )
141 140 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐾 ‘ ( 𝑘 + 1 ) ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑘 ) ) )
142 139 141 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑘 + 1 ) ) )
143 136 39 40 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝐾 : ℕ ⟶ 𝑈 )
144 108 peano2nnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
145 143 144 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐾 ‘ ( 𝑘 + 1 ) ) ∈ 𝑈 )
146 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ∈ 𝑈 ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
147 115 145 146 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
148 142 147 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
149 148 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) )
150 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) ∈ ℝ )
151 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
152 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → 𝐺 : 𝑈 ⟶ ℕ )
153 143 108 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐾 ‘ 𝑘 ) ∈ 𝑈 )
154 152 153 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ∈ ℕ )
155 151 154 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ∈ ( ℝ × ℝ ) )
156 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ )
157 155 156 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ )
158 152 145 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ∈ ℕ )
159 151 158 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ( ℝ × ℝ ) )
160 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ∈ ℝ )
161 159 160 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ∈ ℝ )
162 lttr ⊢ ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ∈ ℝ ) → ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
163 150 157 161 162 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
164 149 163 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
165 164 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
166 165 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 < 𝑘 → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
167 19 breq1d ⊢ ( 𝑦 = 𝑘 → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
168 149 167 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 = 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) )
169 168 a1dd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 = 𝑘 → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
170 166 169 jaod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 𝑦 < 𝑘 ∨ 𝑦 = 𝑘 ) → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
171 114 170 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( 𝑦 < ( 𝑘 + 1 ) → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
172 171 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 ) ) → ( ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) → ( 𝑦 < ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) )
173 106 172 animpimp2impd ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) → ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 ( 𝑘 + 1 ) ≤ 𝑚 → ( 𝑦 < ( 𝑘 + 1 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑘 + 1 ) ) ) ) ) ) ) ) ) )
174 67 77 87 77 91 173 nnind ⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑚 ∈ 𝑊 𝑘 ≤ 𝑚 → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) ) ) )
175 50 52 57 174 syl3c ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ( 𝑦 < 𝑘 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) ) ) )
176 19 22 25 28 48 175 eqord1 ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑃 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ( 𝑁 = 𝑃 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑃 ) ) ) ) ) )