Metamath Proof Explorer

Theorem ovolicc2lem3

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

Ref Expression
Hypotheses ovolicc.1 ${⊢}{\phi }\to {A}\in ℝ$
ovolicc.2 ${⊢}{\phi }\to {B}\in ℝ$
ovolicc.3 ${⊢}{\phi }\to {A}\le {B}$
ovolicc2.4 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
ovolicc2.5 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
ovolicc2.6 ${⊢}{\phi }\to {U}\in \left(𝒫\mathrm{ran}\left(\left(.\right)\circ {F}\right)\cap \mathrm{Fin}\right)$
ovolicc2.7 ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \bigcup {U}$
ovolicc2.8 ${⊢}{\phi }\to {G}:{U}⟶ℕ$
ovolicc2.9 ${⊢}\left({\phi }\wedge {t}\in {U}\right)\to \left(\left(.\right)\circ {F}\right)\left({G}\left({t}\right)\right)={t}$
ovolicc2.10 ${⊢}{T}=\left\{{u}\in {U}|{u}\cap \left[{A},{B}\right]\ne \varnothing \right\}$
ovolicc2.11 ${⊢}{\phi }\to {H}:{T}⟶{T}$
ovolicc2.12 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)\in {H}\left({t}\right)$
ovolicc2.13 ${⊢}{\phi }\to {A}\in {C}$
ovolicc2.14 ${⊢}{\phi }\to {C}\in {T}$
ovolicc2.15 ${⊢}{K}=seq1\left(\left({H}\circ {1}^{st}\right),\left(ℕ×\left\{{C}\right\}\right)\right)$
ovolicc2.16 ${⊢}{W}=\left\{{n}\in ℕ|{B}\in {K}\left({n}\right)\right\}$
Assertion ovolicc2lem3 ${⊢}\left({\phi }\wedge \left({N}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {P}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to \left({N}={P}↔{2}^{nd}\left({F}\left({G}\left({K}\left({N}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({P}\right)\right)\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 ovolicc.1 ${⊢}{\phi }\to {A}\in ℝ$
2 ovolicc.2 ${⊢}{\phi }\to {B}\in ℝ$
3 ovolicc.3 ${⊢}{\phi }\to {A}\le {B}$
4 ovolicc2.4 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
5 ovolicc2.5 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
6 ovolicc2.6 ${⊢}{\phi }\to {U}\in \left(𝒫\mathrm{ran}\left(\left(.\right)\circ {F}\right)\cap \mathrm{Fin}\right)$
7 ovolicc2.7 ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \bigcup {U}$
8 ovolicc2.8 ${⊢}{\phi }\to {G}:{U}⟶ℕ$
9 ovolicc2.9 ${⊢}\left({\phi }\wedge {t}\in {U}\right)\to \left(\left(.\right)\circ {F}\right)\left({G}\left({t}\right)\right)={t}$
10 ovolicc2.10 ${⊢}{T}=\left\{{u}\in {U}|{u}\cap \left[{A},{B}\right]\ne \varnothing \right\}$
11 ovolicc2.11 ${⊢}{\phi }\to {H}:{T}⟶{T}$
12 ovolicc2.12 ${⊢}\left({\phi }\wedge {t}\in {T}\right)\to if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)\in {H}\left({t}\right)$
13 ovolicc2.13 ${⊢}{\phi }\to {A}\in {C}$
14 ovolicc2.14 ${⊢}{\phi }\to {C}\in {T}$
15 ovolicc2.15 ${⊢}{K}=seq1\left(\left({H}\circ {1}^{st}\right),\left(ℕ×\left\{{C}\right\}\right)\right)$
16 ovolicc2.16 ${⊢}{W}=\left\{{n}\in ℕ|{B}\in {K}\left({n}\right)\right\}$
17 2fveq3 ${⊢}{y}={k}\to {G}\left({K}\left({y}\right)\right)={G}\left({K}\left({k}\right)\right)$
18 17 fveq2d ${⊢}{y}={k}\to {F}\left({G}\left({K}\left({y}\right)\right)\right)={F}\left({G}\left({K}\left({k}\right)\right)\right)$
19 18 fveq2d ${⊢}{y}={k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)$
20 2fveq3 ${⊢}{y}={N}\to {G}\left({K}\left({y}\right)\right)={G}\left({K}\left({N}\right)\right)$
21 20 fveq2d ${⊢}{y}={N}\to {F}\left({G}\left({K}\left({y}\right)\right)\right)={F}\left({G}\left({K}\left({N}\right)\right)\right)$
22 21 fveq2d ${⊢}{y}={N}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({N}\right)\right)\right)\right)$
23 2fveq3 ${⊢}{y}={P}\to {G}\left({K}\left({y}\right)\right)={G}\left({K}\left({P}\right)\right)$
24 23 fveq2d ${⊢}{y}={P}\to {F}\left({G}\left({K}\left({y}\right)\right)\right)={F}\left({G}\left({K}\left({P}\right)\right)\right)$
25 24 fveq2d ${⊢}{y}={P}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({P}\right)\right)\right)\right)$
26 ssrab2 ${⊢}\left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\subseteq ℕ$
27 nnssre ${⊢}ℕ\subseteq ℝ$
28 26 27 sstri ${⊢}\left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\subseteq ℝ$
29 26 sseli ${⊢}{y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\to {y}\in ℕ$
30 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
31 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{2}\right)\to {F}:ℕ⟶{ℝ}^{2}$
32 5 30 31 sylancl ${⊢}{\phi }\to {F}:ℕ⟶{ℝ}^{2}$
33 32 adantr ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {F}:ℕ⟶{ℝ}^{2}$
34 8 adantr ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {G}:{U}⟶ℕ$
35 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
36 1zzd ${⊢}{\phi }\to 1\in ℤ$
37 35 15 36 14 11 algrf ${⊢}{\phi }\to {K}:ℕ⟶{T}$
38 37 adantr ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {K}:ℕ⟶{T}$
39 10 ssrab3 ${⊢}{T}\subseteq {U}$
40 fss ${⊢}\left({K}:ℕ⟶{T}\wedge {T}\subseteq {U}\right)\to {K}:ℕ⟶{U}$
41 38 39 40 sylancl ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {K}:ℕ⟶{U}$
42 ffvelrn ${⊢}\left({K}:ℕ⟶{U}\wedge {y}\in ℕ\right)\to {K}\left({y}\right)\in {U}$
43 41 42 sylancom ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {K}\left({y}\right)\in {U}$
44 34 43 ffvelrnd ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {G}\left({K}\left({y}\right)\right)\in ℕ$
45 33 44 ffvelrnd ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {F}\left({G}\left({K}\left({y}\right)\right)\right)\in {ℝ}^{2}$
46 xp2nd ${⊢}{F}\left({G}\left({K}\left({y}\right)\right)\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)\in ℝ$
47 45 46 syl ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)\in ℝ$
48 29 47 sylan2 ${⊢}\left({\phi }\wedge {y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)\in ℝ$
49 26 sseli ${⊢}{k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\to {k}\in ℕ$
50 49 ad2antll ${⊢}\left({\phi }\wedge \left({y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to {k}\in ℕ$
51 29 anim2i ${⊢}\left({\phi }\wedge {y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\to \left({\phi }\wedge {y}\in ℕ\right)$
52 51 adantrr ${⊢}\left({\phi }\wedge \left({y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to \left({\phi }\wedge {y}\in ℕ\right)$
53 breq1 ${⊢}{n}={k}\to \left({n}\le {m}↔{k}\le {m}\right)$
54 53 ralbidv ${⊢}{n}={k}\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}↔\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\right)$
55 54 elrab ${⊢}{k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}↔\left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\right)$
56 55 simprbi ${⊢}{k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\to \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}$
57 56 ad2antll ${⊢}\left({\phi }\wedge \left({y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}$
58 breq1 ${⊢}{x}=1\to \left({x}\le {m}↔1\le {m}\right)$
59 58 ralbidv ${⊢}{x}=1\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}↔\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}1\le {m}\right)$
60 breq2 ${⊢}{x}=1\to \left({y}<{x}↔{y}<1\right)$
61 2fveq3 ${⊢}{x}=1\to {G}\left({K}\left({x}\right)\right)={G}\left({K}\left(1\right)\right)$
62 61 fveq2d ${⊢}{x}=1\to {F}\left({G}\left({K}\left({x}\right)\right)\right)={F}\left({G}\left({K}\left(1\right)\right)\right)$
63 62 fveq2d ${⊢}{x}=1\to {2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)$
64 63 breq2d ${⊢}{x}=1\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)↔{2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)$
65 60 64 imbi12d ${⊢}{x}=1\to \left(\left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)↔\left({y}<1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)\right)$
66 59 65 imbi12d ${⊢}{x}=1\to \left(\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)↔\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}1\le {m}\to \left({y}<1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)\right)\right)$
67 66 imbi2d ${⊢}{x}=1\to \left(\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)\right)↔\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}1\le {m}\to \left({y}<1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)\right)\right)\right)$
68 breq1 ${⊢}{x}={k}\to \left({x}\le {m}↔{k}\le {m}\right)$
69 68 ralbidv ${⊢}{x}={k}\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}↔\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\right)$
70 breq2 ${⊢}{x}={k}\to \left({y}<{x}↔{y}<{k}\right)$
71 2fveq3 ${⊢}{x}={k}\to {G}\left({K}\left({x}\right)\right)={G}\left({K}\left({k}\right)\right)$
72 71 fveq2d ${⊢}{x}={k}\to {F}\left({G}\left({K}\left({x}\right)\right)\right)={F}\left({G}\left({K}\left({k}\right)\right)\right)$
73 72 fveq2d ${⊢}{x}={k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)$
74 73 breq2d ${⊢}{x}={k}\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)↔{2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)$
75 70 74 imbi12d ${⊢}{x}={k}\to \left(\left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)↔\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)$
76 69 75 imbi12d ${⊢}{x}={k}\to \left(\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)↔\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)$
77 76 imbi2d ${⊢}{x}={k}\to \left(\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)\right)↔\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)\right)$
78 breq1 ${⊢}{x}={k}+1\to \left({x}\le {m}↔{k}+1\le {m}\right)$
79 78 ralbidv ${⊢}{x}={k}+1\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}↔\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)$
80 breq2 ${⊢}{x}={k}+1\to \left({y}<{x}↔{y}<{k}+1\right)$
81 2fveq3 ${⊢}{x}={k}+1\to {G}\left({K}\left({x}\right)\right)={G}\left({K}\left({k}+1\right)\right)$
82 81 fveq2d ${⊢}{x}={k}+1\to {F}\left({G}\left({K}\left({x}\right)\right)\right)={F}\left({G}\left({K}\left({k}+1\right)\right)\right)$
83 82 fveq2d ${⊢}{x}={k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)$
84 83 breq2d ${⊢}{x}={k}+1\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)↔{2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
85 80 84 imbi12d ${⊢}{x}={k}+1\to \left(\left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)↔\left({y}<{k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
86 79 85 imbi12d ${⊢}{x}={k}+1\to \left(\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)↔\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({y}<{k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)\right)$
87 86 imbi2d ${⊢}{x}={k}+1\to \left(\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{x}\le {m}\to \left({y}<{x}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({x}\right)\right)\right)\right)\right)\right)\right)↔\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({y}<{k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)\right)\right)$
88 nnnlt1 ${⊢}{y}\in ℕ\to ¬{y}<1$
89 88 adantl ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to ¬{y}<1$
90 89 pm2.21d ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to \left({y}<1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)$
91 90 a1d ${⊢}\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}1\le {m}\to \left({y}<1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left(1\right)\right)\right)\right)\right)\right)$
92 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
93 92 adantr ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to {k}\in ℝ$
94 93 lep1d ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to {k}\le {k}+1$
95 peano2re ${⊢}{k}\in ℝ\to {k}+1\in ℝ$
96 93 95 syl ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to {k}+1\in ℝ$
97 16 ssrab3 ${⊢}{W}\subseteq ℕ$
98 97 27 sstri ${⊢}{W}\subseteq ℝ$
99 98 sseli ${⊢}{m}\in {W}\to {m}\in ℝ$
100 99 adantl ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to {m}\in ℝ$
101 letr ${⊢}\left({k}\in ℝ\wedge {k}+1\in ℝ\wedge {m}\in ℝ\right)\to \left(\left({k}\le {k}+1\wedge {k}+1\le {m}\right)\to {k}\le {m}\right)$
102 93 96 100 101 syl3anc ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to \left(\left({k}\le {k}+1\wedge {k}+1\le {m}\right)\to {k}\le {m}\right)$
103 94 102 mpand ${⊢}\left({k}\in ℕ\wedge {m}\in {W}\right)\to \left({k}+1\le {m}\to {k}\le {m}\right)$
104 103 ralimdva ${⊢}{k}\in ℕ\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\right)$
105 104 imim1d ${⊢}{k}\in ℕ\to \left(\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)$
106 105 adantl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge {k}\in ℕ\right)\to \left(\left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)$
107 simplr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {y}\in ℕ$
108 simprl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {k}\in ℕ$
109 nnleltp1 ${⊢}\left({y}\in ℕ\wedge {k}\in ℕ\right)\to \left({y}\le {k}↔{y}<{k}+1\right)$
110 107 108 109 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}\le {k}↔{y}<{k}+1\right)$
111 107 nnred ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {y}\in ℝ$
112 108 nnred ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {k}\in ℝ$
113 111 112 leloed ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}\le {k}↔\left({y}<{k}\vee {y}={k}\right)\right)$
114 110 113 bitr3d ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}<{k}+1↔\left({y}<{k}\vee {y}={k}\right)\right)$
115 simpll ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {\phi }$
116 ltp1 ${⊢}{k}\in ℝ\to {k}<{k}+1$
117 ltnle ${⊢}\left({k}\in ℝ\wedge {k}+1\in ℝ\right)\to \left({k}<{k}+1↔¬{k}+1\le {k}\right)$
118 95 117 mpdan ${⊢}{k}\in ℝ\to \left({k}<{k}+1↔¬{k}+1\le {k}\right)$
119 116 118 mpbid ${⊢}{k}\in ℝ\to ¬{k}+1\le {k}$
120 112 119 syl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to ¬{k}+1\le {k}$
121 breq2 ${⊢}{m}={k}\to \left({k}+1\le {m}↔{k}+1\le {k}\right)$
122 121 rspccv ${⊢}\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({k}\in {W}\to {k}+1\le {k}\right)$
123 122 ad2antll ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({k}\in {W}\to {k}+1\le {k}\right)$
124 120 123 mtod ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to ¬{k}\in {W}$
125 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 ${⊢}\left({\phi }\wedge \left({k}\in ℕ\wedge ¬{k}\in {W}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B}$
126 115 108 124 125 syl12anc ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B}$
127 126 iftrued ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to if\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right),{B}\right)={2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)$
128 2fveq3 ${⊢}{t}={K}\left({k}\right)\to {F}\left({G}\left({t}\right)\right)={F}\left({G}\left({K}\left({k}\right)\right)\right)$
129 128 fveq2d ${⊢}{t}={K}\left({k}\right)\to {2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)$
130 129 breq1d ${⊢}{t}={K}\left({k}\right)\to \left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B}↔{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B}\right)$
131 130 129 ifbieq1d ${⊢}{t}={K}\left({k}\right)\to if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)=if\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right),{B}\right)$
132 fveq2 ${⊢}{t}={K}\left({k}\right)\to {H}\left({t}\right)={H}\left({K}\left({k}\right)\right)$
133 131 132 eleq12d ${⊢}{t}={K}\left({k}\right)\to \left(if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)\in {H}\left({t}\right)↔if\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right),{B}\right)\in {H}\left({K}\left({k}\right)\right)\right)$
134 12 ralrimiva ${⊢}{\phi }\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)\in {H}\left({t}\right)$
135 134 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}if\left({2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({t}\right)\right)\right),{B}\right)\in {H}\left({t}\right)$
136 37 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}:ℕ⟶{T}$
137 136 108 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}\left({k}\right)\in {T}$
138 133 135 137 rspcdva ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to if\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\le {B},{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right),{B}\right)\in {H}\left({K}\left({k}\right)\right)$
139 127 138 eqeltrrd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in {H}\left({K}\left({k}\right)\right)$
140 35 15 36 14 11 algrp1 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {K}\left({k}+1\right)={H}\left({K}\left({k}\right)\right)$
141 140 ad2ant2r ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}\left({k}+1\right)={H}\left({K}\left({k}\right)\right)$
142 139 141 eleqtrrd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in {K}\left({k}+1\right)$
143 136 39 40 sylancl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}:ℕ⟶{U}$
144 108 peano2nnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {k}+1\in ℕ$
145 143 144 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}\left({k}+1\right)\in {U}$
146 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ${⊢}\left({\phi }\wedge {K}\left({k}+1\right)\in {U}\right)\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in {K}\left({k}+1\right)↔\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
147 115 145 146 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in {K}\left({k}+1\right)↔\left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
148 142 147 mpbid ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
149 148 simp3d ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)$
150 47 adantr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)\in ℝ$
151 32 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {F}:ℕ⟶{ℝ}^{2}$
152 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {G}:{U}⟶ℕ$
153 143 108 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {K}\left({k}\right)\in {U}$
154 152 153 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {G}\left({K}\left({k}\right)\right)\in ℕ$
155 151 154 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {F}\left({G}\left({K}\left({k}\right)\right)\right)\in {ℝ}^{2}$
156 xp2nd ${⊢}{F}\left({G}\left({K}\left({k}\right)\right)\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ$
157 155 156 syl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ$
158 152 145 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {G}\left({K}\left({k}+1\right)\right)\in ℕ$
159 151 158 ffvelrnd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {F}\left({G}\left({K}\left({k}+1\right)\right)\right)\in {ℝ}^{2}$
160 xp2nd ${⊢}{F}\left({G}\left({K}\left({k}+1\right)\right)\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\in ℝ$
161 159 160 syl ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\in ℝ$
162 lttr ${⊢}\left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\in ℝ\right)\to \left(\left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
163 150 157 161 162 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left(\left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\wedge {2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
164 149 163 mpan2d ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
165 164 imim2d ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
166 165 com23 ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}<{k}\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
167 19 breq1d ${⊢}{y}={k}\to \left({2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)↔{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
168 149 167 syl5ibrcom ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}={k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)$
169 168 a1dd ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}={k}\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
170 166 169 jaod ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left(\left({y}<{k}\vee {y}={k}\right)\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
171 114 170 sylbid ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left({y}<{k}+1\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
172 171 com23 ${⊢}\left(\left({\phi }\wedge {y}\in ℕ\right)\wedge \left({k}\in ℕ\wedge \forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\right)\right)\to \left(\left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\to \left({y}<{k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)$
173 106 172 animpimp2impd ${⊢}{k}\in ℕ\to \left(\left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)\to \left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}+1\le {m}\to \left({y}<{k}+1\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}+1\right)\right)\right)\right)\right)\right)\right)\right)$
174 67 77 87 77 91 173 nnind ${⊢}{k}\in ℕ\to \left(\left({\phi }\wedge {y}\in ℕ\right)\to \left(\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{k}\le {m}\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)\right)\right)$
175 50 52 57 174 syl3c ${⊢}\left({\phi }\wedge \left({y}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {k}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to \left({y}<{k}\to {2}^{nd}\left({F}\left({G}\left({K}\left({y}\right)\right)\right)\right)<{2}^{nd}\left({F}\left({G}\left({K}\left({k}\right)\right)\right)\right)\right)$
176 19 22 25 28 48 175 eqord1 ${⊢}\left({\phi }\wedge \left({N}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\wedge {P}\in \left\{{n}\in ℕ|\forall {m}\in {W}\phantom{\rule{.4em}{0ex}}{n}\le {m}\right\}\right)\right)\to \left({N}={P}↔{2}^{nd}\left({F}\left({G}\left({K}\left({N}\right)\right)\right)\right)={2}^{nd}\left({F}\left({G}\left({K}\left({P}\right)\right)\right)\right)\right)$