# Metamath Proof Explorer

## Theorem vdwlem13

Description: Lemma for vdw . Main induction on K ; K = 0 , K = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
vdw.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
Assertion vdwlem13 ${⊢}{\phi }\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}$

### Proof

Step Hyp Ref Expression
1 vdw.r ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
2 vdw.k ${⊢}{\phi }\to {K}\in {ℕ}_{0}$
3 elnn1uz2 ${⊢}{K}\in ℕ↔\left({K}=1\vee {K}\in {ℤ}_{\ge 2}\right)$
4 ovex ${⊢}\left(1\dots 1\right)\in \mathrm{V}$
5 elmapg ${⊢}\left({R}\in \mathrm{Fin}\wedge \left(1\dots 1\right)\in \mathrm{V}\right)\to \left({f}\in \left({{R}}^{\left(1\dots 1\right)}\right)↔{f}:\left(1\dots 1\right)⟶{R}\right)$
6 1 4 5 sylancl ${⊢}{\phi }\to \left({f}\in \left({{R}}^{\left(1\dots 1\right)}\right)↔{f}:\left(1\dots 1\right)⟶{R}\right)$
7 6 biimpa ${⊢}\left({\phi }\wedge {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\right)\to {f}:\left(1\dots 1\right)⟶{R}$
8 1nn ${⊢}1\in ℕ$
9 vdwap1 ${⊢}\left(1\in ℕ\wedge 1\in ℕ\right)\to 1\mathrm{AP}\left(1\right)1=\left\{1\right\}$
10 8 8 9 mp2an ${⊢}1\mathrm{AP}\left(1\right)1=\left\{1\right\}$
11 1z ${⊢}1\in ℤ$
12 elfz3 ${⊢}1\in ℤ\to 1\in \left(1\dots 1\right)$
13 11 12 mp1i ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to 1\in \left(1\dots 1\right)$
14 eqidd ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to {f}\left(1\right)={f}\left(1\right)$
15 ffn ${⊢}{f}:\left(1\dots 1\right)⟶{R}\to {f}Fn\left(1\dots 1\right)$
16 15 adantl ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to {f}Fn\left(1\dots 1\right)$
17 fniniseg ${⊢}{f}Fn\left(1\dots 1\right)\to \left(1\in {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔\left(1\in \left(1\dots 1\right)\wedge {f}\left(1\right)={f}\left(1\right)\right)\right)$
18 16 17 syl ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to \left(1\in {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔\left(1\in \left(1\dots 1\right)\wedge {f}\left(1\right)={f}\left(1\right)\right)\right)$
19 13 14 18 mpbir2and ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to 1\in {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
20 19 snssd ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to \left\{1\right\}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
21 10 20 eqsstrid ${⊢}\left({\phi }\wedge {f}:\left(1\dots 1\right)⟶{R}\right)\to 1\mathrm{AP}\left(1\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
22 7 21 syldan ${⊢}\left({\phi }\wedge {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\right)\to 1\mathrm{AP}\left(1\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
23 22 ralrimiva ${⊢}{\phi }\to \forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left(1\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
24 fveq2 ${⊢}{K}=1\to \mathrm{AP}\left({K}\right)=\mathrm{AP}\left(1\right)$
25 24 oveqd ${⊢}{K}=1\to 1\mathrm{AP}\left({K}\right)1=1\mathrm{AP}\left(1\right)1$
26 25 sseq1d ${⊢}{K}=1\to \left(1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔1\mathrm{AP}\left(1\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
27 26 ralbidv ${⊢}{K}=1\to \left(\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left(1\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
28 23 27 syl5ibrcom ${⊢}{\phi }\to \left({K}=1\to \forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
29 oveq1 ${⊢}{a}=1\to {a}\mathrm{AP}\left({K}\right){d}=1\mathrm{AP}\left({K}\right){d}$
30 29 sseq1d ${⊢}{a}=1\to \left({a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔1\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
31 oveq2 ${⊢}{d}=1\to 1\mathrm{AP}\left({K}\right){d}=1\mathrm{AP}\left({K}\right)1$
32 31 sseq1d ${⊢}{d}=1\to \left(1\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]↔1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
33 30 32 rspc2ev ${⊢}\left(1\in ℕ\wedge 1\in ℕ\wedge 1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
34 8 8 33 mp3an12 ${⊢}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
35 fvex ${⊢}{f}\left(1\right)\in \mathrm{V}$
36 sneq ${⊢}{c}={f}\left(1\right)\to \left\{{c}\right\}=\left\{{f}\left(1\right)\right\}$
37 36 imaeq2d ${⊢}{c}={f}\left(1\right)\to {{f}}^{-1}\left[\left\{{c}\right\}\right]={{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
38 37 sseq2d ${⊢}{c}={f}\left(1\right)\to \left({a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]↔{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
39 38 2rexbidv ${⊢}{c}={f}\left(1\right)\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\right)$
40 35 39 spcev ${⊢}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to \exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]$
41 34 40 syl ${⊢}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to \exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]$
42 2 adantr ${⊢}\left({\phi }\wedge {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\right)\to {K}\in {ℕ}_{0}$
43 4 42 7 vdwmc ${⊢}\left({\phi }\wedge {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\right)\to \left({K}\mathrm{MonoAP}{f}↔\exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left({K}\right){d}\subseteq {{f}}^{-1}\left[\left\{{c}\right\}\right]\right)$
44 41 43 syl5ibr ${⊢}\left({\phi }\wedge {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\right)\to \left(1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to {K}\mathrm{MonoAP}{f}\right)$
45 44 ralimdva ${⊢}{\phi }\to \left(\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to \forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
46 oveq2 ${⊢}{n}=1\to \left(1\dots {n}\right)=\left(1\dots 1\right)$
47 46 oveq2d ${⊢}{n}=1\to {{R}}^{\left(1\dots {n}\right)}={{R}}^{\left(1\dots 1\right)}$
48 47 raleqdv ${⊢}{n}=1\to \left(\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}↔\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
49 48 rspcev ${⊢}\left(1\in ℕ\wedge \forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}$
50 8 49 mpan ${⊢}\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}$
51 45 50 syl6 ${⊢}{\phi }\to \left(\forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
52 28 51 syld ${⊢}{\phi }\to \left({K}=1\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
53 breq1 ${⊢}{x}=2\to \left({x}\mathrm{MonoAP}{f}↔2\mathrm{MonoAP}{f}\right)$
54 53 rexralbidv ${⊢}{x}=2\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}\right)$
55 54 ralbidv ${⊢}{x}=2\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}\right)$
56 breq1 ${⊢}{x}={k}\to \left({x}\mathrm{MonoAP}{f}↔{k}\mathrm{MonoAP}{f}\right)$
57 56 rexralbidv ${⊢}{x}={k}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\right)$
58 57 ralbidv ${⊢}{x}={k}\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\right)$
59 breq1 ${⊢}{x}={k}+1\to \left({x}\mathrm{MonoAP}{f}↔\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
60 59 rexralbidv ${⊢}{x}={k}+1\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
61 60 ralbidv ${⊢}{x}={k}+1\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
62 breq1 ${⊢}{x}={K}\to \left({x}\mathrm{MonoAP}{f}↔{K}\mathrm{MonoAP}{f}\right)$
63 62 rexralbidv ${⊢}{x}={K}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
64 63 ralbidv ${⊢}{x}={K}\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{x}\mathrm{MonoAP}{f}↔\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
65 hashcl ${⊢}{r}\in \mathrm{Fin}\to \left|{r}\right|\in {ℕ}_{0}$
66 nn0p1nn ${⊢}\left|{r}\right|\in {ℕ}_{0}\to \left|{r}\right|+1\in ℕ$
67 65 66 syl ${⊢}{r}\in \mathrm{Fin}\to \left|{r}\right|+1\in ℕ$
68 simpll ${⊢}\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)\to {r}\in \mathrm{Fin}$
69 simplr ${⊢}\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)\to {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)$
70 vex ${⊢}{r}\in \mathrm{V}$
71 ovex ${⊢}\left(1\dots \left|{r}\right|+1\right)\in \mathrm{V}$
72 70 71 elmap ${⊢}{f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)↔{f}:\left(1\dots \left|{r}\right|+1\right)⟶{r}$
73 69 72 sylib ${⊢}\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)\to {f}:\left(1\dots \left|{r}\right|+1\right)⟶{r}$
74 simpr ${⊢}\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)\to ¬2\mathrm{MonoAP}{f}$
75 68 73 74 vdwlem12 ${⊢}¬\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)$
76 iman ${⊢}\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\to 2\mathrm{MonoAP}{f}\right)↔¬\left(\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\wedge ¬2\mathrm{MonoAP}{f}\right)$
77 75 76 mpbir ${⊢}\left({r}\in \mathrm{Fin}\wedge {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\right)\to 2\mathrm{MonoAP}{f}$
78 77 ralrimiva ${⊢}{r}\in \mathrm{Fin}\to \forall {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}$
79 oveq2 ${⊢}{n}=\left|{r}\right|+1\to \left(1\dots {n}\right)=\left(1\dots \left|{r}\right|+1\right)$
80 79 oveq2d ${⊢}{n}=\left|{r}\right|+1\to {{r}}^{\left(1\dots {n}\right)}={{r}}^{\left(1\dots \left|{r}\right|+1\right)}$
81 80 raleqdv ${⊢}{n}=\left|{r}\right|+1\to \left(\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}↔\forall {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}\right)$
82 81 rspcev ${⊢}\left(\left|{r}\right|+1\in ℕ\wedge \forall {f}\in \left({{r}}^{\left(1\dots \left|{r}\right|+1\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}$
83 67 78 82 syl2anc ${⊢}{r}\in \mathrm{Fin}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}$
84 83 rgen ${⊢}\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}2\mathrm{MonoAP}{f}$
85 oveq1 ${⊢}{r}={s}\to {{r}}^{\left(1\dots {n}\right)}={{s}}^{\left(1\dots {n}\right)}$
86 85 raleqdv ${⊢}{r}={s}\to \left(\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\right)$
87 86 rexbidv ${⊢}{r}={s}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\right)$
88 oveq2 ${⊢}{n}={m}\to \left(1\dots {n}\right)=\left(1\dots {m}\right)$
89 88 oveq2d ${⊢}{n}={m}\to {{s}}^{\left(1\dots {n}\right)}={{s}}^{\left(1\dots {m}\right)}$
90 89 raleqdv ${⊢}{n}={m}\to \left(\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {f}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\right)$
91 breq2 ${⊢}{f}={g}\to \left({k}\mathrm{MonoAP}{f}↔{k}\mathrm{MonoAP}{g}\right)$
92 91 cbvralvw ${⊢}\forall {f}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}$
93 90 92 syl6bb ${⊢}{n}={m}\to \left(\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)$
94 93 cbvrexvw ${⊢}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}$
95 87 94 syl6bb ${⊢}{r}={s}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)$
96 95 cbvralvw ${⊢}\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}$
97 simplr ${⊢}\left(\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\wedge \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)\to {r}\in \mathrm{Fin}$
98 simpll ${⊢}\left(\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\wedge \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)\to {k}\in {ℤ}_{\ge 2}$
99 simpr ${⊢}\left(\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\wedge \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)\to \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}$
100 94 ralbii ${⊢}\forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}↔\forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}$
101 99 100 sylibr ${⊢}\left(\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\wedge \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)\to \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{s}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}$
102 97 98 101 vdwlem11 ${⊢}\left(\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\wedge \forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}$
103 102 ex ${⊢}\left({k}\in {ℤ}_{\ge 2}\wedge {r}\in \mathrm{Fin}\right)\to \left(\forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
104 103 ralrimdva ${⊢}{k}\in {ℤ}_{\ge 2}\to \left(\forall {s}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({{s}}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{g}\to \forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
105 96 104 syl5bi ${⊢}{k}\in {ℤ}_{\ge 2}\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{k}\mathrm{MonoAP}{f}\to \forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({k}+1\right)\mathrm{MonoAP}{f}\right)$
106 55 58 61 64 84 105 uzind4i ${⊢}{K}\in {ℤ}_{\ge 2}\to \forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}$
107 oveq1 ${⊢}{r}={R}\to {{r}}^{\left(1\dots {n}\right)}={{R}}^{\left(1\dots {n}\right)}$
108 107 raleqdv ${⊢}{r}={R}\to \left(\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}↔\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
109 108 rexbidv ${⊢}{r}={R}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
110 109 rspcv ${⊢}{R}\in \mathrm{Fin}\to \left(\forall {r}\in \mathrm{Fin}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{r}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
111 1 106 110 syl2im ${⊢}{\phi }\to \left({K}\in {ℤ}_{\ge 2}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
112 52 111 jaod ${⊢}{\phi }\to \left(\left({K}=1\vee {K}\in {ℤ}_{\ge 2}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
113 3 112 syl5bi ${⊢}{\phi }\to \left({K}\in ℕ\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
114 fveq2 ${⊢}{K}=0\to \mathrm{AP}\left({K}\right)=\mathrm{AP}\left(0\right)$
115 114 oveqd ${⊢}{K}=0\to 1\mathrm{AP}\left({K}\right)1=1\mathrm{AP}\left(0\right)1$
116 vdwap0 ${⊢}\left(1\in ℕ\wedge 1\in ℕ\right)\to 1\mathrm{AP}\left(0\right)1=\varnothing$
117 8 8 116 mp2an ${⊢}1\mathrm{AP}\left(0\right)1=\varnothing$
118 115 117 syl6eq ${⊢}{K}=0\to 1\mathrm{AP}\left({K}\right)1=\varnothing$
119 0ss ${⊢}\varnothing \subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
120 118 119 eqsstrdi ${⊢}{K}=0\to 1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
121 120 ralrimivw ${⊢}{K}=0\to \forall {f}\in \left({{R}}^{\left(1\dots 1\right)}\right)\phantom{\rule{.4em}{0ex}}1\mathrm{AP}\left({K}\right)1\subseteq {{f}}^{-1}\left[\left\{{f}\left(1\right)\right\}\right]$
122 121 51 syl5 ${⊢}{\phi }\to \left({K}=0\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}\right)$
123 elnn0 ${⊢}{K}\in {ℕ}_{0}↔\left({K}\in ℕ\vee {K}=0\right)$
124 2 123 sylib ${⊢}{\phi }\to \left({K}\in ℕ\vee {K}=0\right)$
125 113 122 124 mpjaod ${⊢}{\phi }\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({{R}}^{\left(1\dots {n}\right)}\right)\phantom{\rule{.4em}{0ex}}{K}\mathrm{MonoAP}{f}$