Metamath Proof Explorer

Theorem vdwlem10

Description: Lemma for vdw . Set up secondary induction on M . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r 
|- ( ph -> R e. Fin )
vdwlem9.k 
|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem9.s 
|- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
vdwlem10.m 
|- ( ph -> M e. NN )
Assertion vdwlem10 
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )

Proof

Step Hyp Ref Expression
1 vdw.r 
 |-  ( ph -> R e. Fin )
2 vdwlem9.k 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
3 vdwlem9.s 
 |-  ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
4 vdwlem10.m 
 |-  ( ph -> M e. NN )
5 opeq1 
 |-  ( x = 1 -> <. x , K >. = <. 1 , K >. )
6 5 breq1d 
 |-  ( x = 1 -> ( <. x , K >. PolyAP f <-> <. 1 , K >. PolyAP f ) )
7 6 orbi1d 
 |-  ( x = 1 -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
8 7 rexralbidv 
 |-  ( x = 1 -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
9 8 imbi2d 
 |-  ( x = 1 -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
10 opeq1 
 |-  ( x = m -> <. x , K >. = <. m , K >. )
11 10 breq1d 
 |-  ( x = m -> ( <. x , K >. PolyAP f <-> <. m , K >. PolyAP f ) )
12 11 orbi1d 
 |-  ( x = m -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
13 12 rexralbidv 
 |-  ( x = m -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
14 13 imbi2d 
 |-  ( x = m -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
15 opeq1 
 |-  ( x = ( m + 1 ) -> <. x , K >. = <. ( m + 1 ) , K >. )
16 15 breq1d 
 |-  ( x = ( m + 1 ) -> ( <. x , K >. PolyAP f <-> <. ( m + 1 ) , K >. PolyAP f ) )
17 16 orbi1d 
 |-  ( x = ( m + 1 ) -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
18 17 rexralbidv 
 |-  ( x = ( m + 1 ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
19 18 imbi2d 
 |-  ( x = ( m + 1 ) -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
20 opeq1 
 |-  ( x = M -> <. x , K >. = <. M , K >. )
21 20 breq1d 
 |-  ( x = M -> ( <. x , K >. PolyAP f <-> <. M , K >. PolyAP f ) )
22 21 orbi1d 
 |-  ( x = M -> ( ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
23 22 rexralbidv 
 |-  ( x = M -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
24 23 imbi2d 
 |-  ( x = M -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. x , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) <-> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
25 oveq1 
 |-  ( s = R -> ( s ^m ( 1 ... n ) ) = ( R ^m ( 1 ... n ) ) )
26 25 raleqdv 
 |-  ( s = R -> ( A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f ) )
27 26 rexbidv 
 |-  ( s = R -> ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f ) )
28 27 3 1 rspcdva 
 |-  ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f )
29 oveq2 
 |-  ( n = w -> ( 1 ... n ) = ( 1 ... w ) )
30 29 oveq2d 
 |-  ( n = w -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... w ) ) )
31 30 raleqdv 
 |-  ( n = w -> ( A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f ) )
32 31 cbvrexvw 
 |-  ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f )
33 28 32 sylib 
 |-  ( ph -> E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f )
34 breq2 
 |-  ( f = g -> ( K MonoAP f <-> K MonoAP g ) )
35 34 cbvralvw 
 |-  ( A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f <-> A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g )
36 2nn 
 |-  2 e. NN
37 simpr 
 |-  ( ( ph /\ w e. NN ) -> w e. NN )
38 nnmulcl 
 |-  ( ( 2 e. NN /\ w e. NN ) -> ( 2 x. w ) e. NN )
39 36 37 38 sylancr 
 |-  ( ( ph /\ w e. NN ) -> ( 2 x. w ) e. NN )
40 1 adantr 
 |-  ( ( ph /\ w e. NN ) -> R e. Fin )
41 ovex 
 |-  ( 1 ... ( 2 x. w ) ) e. _V
42 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... ( 2 x. w ) ) e. _V ) -> ( f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) <-> f : ( 1 ... ( 2 x. w ) ) --> R ) )
43 40 41 42 sylancl 
 |-  ( ( ph /\ w e. NN ) -> ( f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) <-> f : ( 1 ... ( 2 x. w ) ) --> R ) )
44 43 biimpa 
 |-  ( ( ( ph /\ w e. NN ) /\ f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R )
45 simplr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R )
46 elfznn 
 |-  ( y e. ( 1 ... w ) -> y e. NN )
47 46 adantl 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y e. NN )
48 47 nnred 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y e. RR )
49 simpllr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. NN )
50 49 nnred 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. RR )
51 elfzle2 
 |-  ( y e. ( 1 ... w ) -> y <_ w )
52 51 adantl 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> y <_ w )
53 48 50 50 52 leadd1dd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) <_ ( w + w ) )
54 49 nncnd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> w e. CC )
55 54 2timesd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) = ( w + w ) )
56 53 55 breqtrrd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) <_ ( 2 x. w ) )
57 47 49 nnaddcld 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. NN )
58 nnuz 
 |-  NN = ( ZZ>= ` 1 )
59 57 58 eleqtrdi 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. ( ZZ>= ` 1 ) )
60 39 ad2antrr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) e. NN )
61 60 nnzd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( 2 x. w ) e. ZZ )
62 elfz5 
 |-  ( ( ( y + w ) e. ( ZZ>= ` 1 ) /\ ( 2 x. w ) e. ZZ ) -> ( ( y + w ) e. ( 1 ... ( 2 x. w ) ) <-> ( y + w ) <_ ( 2 x. w ) ) )
63 59 61 62 syl2anc 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( ( y + w ) e. ( 1 ... ( 2 x. w ) ) <-> ( y + w ) <_ ( 2 x. w ) ) )
64 56 63 mpbird 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( y + w ) e. ( 1 ... ( 2 x. w ) ) )
65 45 64 ffvelrnd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ y e. ( 1 ... w ) ) -> ( f ` ( y + w ) ) e. R )
66 fvoveq1 
 |-  ( x = y -> ( f ` ( x + w ) ) = ( f ` ( y + w ) ) )
67 66 cbvmptv 
 |-  ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) = ( y e. ( 1 ... w ) |-> ( f ` ( y + w ) ) )
68 65 67 fmptd 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R )
69 ovex 
 |-  ( 1 ... w ) e. _V
70 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... w ) e. _V ) -> ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) <-> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) )
71 40 69 70 sylancl 
 |-  ( ( ph /\ w e. NN ) -> ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) <-> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) )
72 71 biimpar 
 |-  ( ( ( ph /\ w e. NN ) /\ ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) : ( 1 ... w ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) )
73 68 72 syldan 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) )
74 breq2 
 |-  ( g = ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) -> ( K MonoAP g <-> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) )
75 74 rspcv 
 |-  ( ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) e. ( R ^m ( 1 ... w ) ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) )
76 73 75 syl 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) ) )
77 2nn0 
 |-  2 e. NN0
78 2 ad2antrr 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> K e. ( ZZ>= ` 2 ) )
79 eluznn0 
 |-  ( ( 2 e. NN0 /\ K e. ( ZZ>= ` 2 ) ) -> K e. NN0 )
80 77 78 79 sylancr 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> K e. NN0 )
81 69 80 68 vdwmc 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) <-> E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) )
82 40 ad2antrr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> R e. Fin )
83 78 adantr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> K e. ( ZZ>= ` 2 ) )
84 simpllr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> w e. NN )
85 simplr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> f : ( 1 ... ( 2 x. w ) ) --> R )
86 vex 
 |-  c e. _V
87 simprll 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> a e. NN )
88 simprlr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> d e. NN )
89 simprr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) )
90 82 83 84 85 86 87 88 89 67 vdwlem8 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> <. 1 , K >. PolyAP f )
91 90 orcd 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( ( a e. NN /\ d e. NN ) /\ ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) ) ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
92 91 expr 
 |-  ( ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) /\ ( a e. NN /\ d e. NN ) ) -> ( ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
93 92 rexlimdvva 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
94 93 exlimdv 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( E. c E. a e. NN E. d e. NN ( a ( AP ` K ) d ) C_ ( `' ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) " { c } ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
95 81 94 sylbid 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( K MonoAP ( x e. ( 1 ... w ) |-> ( f ` ( x + w ) ) ) -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
96 76 95 syld 
 |-  ( ( ( ph /\ w e. NN ) /\ f : ( 1 ... ( 2 x. w ) ) --> R ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
97 44 96 syldan 
 |-  ( ( ( ph /\ w e. NN ) /\ f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
98 97 ralrimdva 
 |-  ( ( ph /\ w e. NN ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
99 oveq2 
 |-  ( n = ( 2 x. w ) -> ( 1 ... n ) = ( 1 ... ( 2 x. w ) ) )
100 99 oveq2d 
 |-  ( n = ( 2 x. w ) -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... ( 2 x. w ) ) ) )
101 100 raleqdv 
 |-  ( n = ( 2 x. w ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
102 101 rspcev 
 |-  ( ( ( 2 x. w ) e. NN /\ A. f e. ( R ^m ( 1 ... ( 2 x. w ) ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
103 39 98 102 syl6an 
 |-  ( ( ph /\ w e. NN ) -> ( A. g e. ( R ^m ( 1 ... w ) ) K MonoAP g -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
104 35 103 syl5bi 
 |-  ( ( ph /\ w e. NN ) -> ( A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
105 104 rexlimdva 
 |-  ( ph -> ( E. w e. NN A. f e. ( R ^m ( 1 ... w ) ) K MonoAP f -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
106 33 105 mpd 
 |-  ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. 1 , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
107 breq2 
 |-  ( f = g -> ( <. m , K >. PolyAP f <-> <. m , K >. PolyAP g ) )
108 breq2 
 |-  ( f = g -> ( ( K + 1 ) MonoAP f <-> ( K + 1 ) MonoAP g ) )
109 107 108 orbi12d 
 |-  ( f = g -> ( ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) )
110 109 cbvralvw 
 |-  ( A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. g e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
111 30 raleqdv 
 |-  ( n = w -> ( A. g e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) )
112 110 111 syl5bb 
 |-  ( n = w -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) )
113 112 cbvrexvw 
 |-  ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> E. w e. NN A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
114 oveq2 
 |-  ( n = v -> ( 1 ... n ) = ( 1 ... v ) )
115 114 oveq2d 
 |-  ( n = v -> ( s ^m ( 1 ... n ) ) = ( s ^m ( 1 ... v ) ) )
116 115 raleqdv 
 |-  ( n = v -> ( A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f ) )
117 116 cbvrexvw 
 |-  ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. v e. NN A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f )
118 oveq1 
 |-  ( s = ( R ^m ( 1 ... w ) ) -> ( s ^m ( 1 ... v ) ) = ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) )
119 118 raleqdv 
 |-  ( s = ( R ^m ( 1 ... w ) ) -> ( A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f <-> A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) )
120 119 rexbidv 
 |-  ( s = ( R ^m ( 1 ... w ) ) -> ( E. v e. NN A. f e. ( s ^m ( 1 ... v ) ) K MonoAP f <-> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) )
121 117 120 syl5bb 
 |-  ( s = ( R ^m ( 1 ... w ) ) -> ( E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f <-> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) )
122 3 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
123 1 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> R e. Fin )
124 fzfi 
 |-  ( 1 ... w ) e. Fin
125 mapfi 
 |-  ( ( R e. Fin /\ ( 1 ... w ) e. Fin ) -> ( R ^m ( 1 ... w ) ) e. Fin )
126 123 124 125 sylancl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> ( R ^m ( 1 ... w ) ) e. Fin )
127 121 122 126 rspcdva 
 |-  ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> E. v e. NN A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f )
128 simprll 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> w e. NN )
129 simprrl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> v e. NN )
130 nnmulcl 
 |-  ( ( 2 e. NN /\ v e. NN ) -> ( 2 x. v ) e. NN )
131 36 130 mpan 
 |-  ( v e. NN -> ( 2 x. v ) e. NN )
132 nnmulcl 
 |-  ( ( w e. NN /\ ( 2 x. v ) e. NN ) -> ( w x. ( 2 x. v ) ) e. NN )
133 131 132 sylan2 
 |-  ( ( w e. NN /\ v e. NN ) -> ( w x. ( 2 x. v ) ) e. NN )
134 128 129 133 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> ( w x. ( 2 x. v ) ) e. NN )
135 simp1l 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ph )
136 135 1 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> R e. Fin )
137 135 2 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> K e. ( ZZ>= ` 2 ) )
138 135 3 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
139 simp1r 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> m e. NN )
140 simp2ll 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> w e. NN )
141 simp2lr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
142 breq2 
 |-  ( g = k -> ( <. m , K >. PolyAP g <-> <. m , K >. PolyAP k ) )
143 breq2 
 |-  ( g = k -> ( ( K + 1 ) MonoAP g <-> ( K + 1 ) MonoAP k ) )
144 142 143 orbi12d 
 |-  ( g = k -> ( ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) ) )
145 144 cbvralvw 
 |-  ( A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) <-> A. k e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) )
146 141 145 sylib 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. k e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP k \/ ( K + 1 ) MonoAP k ) )
147 simp2rl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> v e. NN )
148 simp2rr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f )
149 simp3 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) )
150 ovex 
 |-  ( 1 ... ( w x. ( 2 x. v ) ) ) e. _V
151 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... ( w x. ( 2 x. v ) ) ) e. _V ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) <-> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R ) )
152 136 150 151 sylancl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) <-> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R ) )
153 149 152 mpbid 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> h : ( 1 ... ( w x. ( 2 x. v ) ) ) --> R )
154 fvoveq1 
 |-  ( y = u -> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) = ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) )
155 154 cbvmptv 
 |-  ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) )
156 oveq1 
 |-  ( x = z -> ( x - 1 ) = ( z - 1 ) )
157 156 oveq1d 
 |-  ( x = z -> ( ( x - 1 ) + v ) = ( ( z - 1 ) + v ) )
158 157 oveq2d 
 |-  ( x = z -> ( w x. ( ( x - 1 ) + v ) ) = ( w x. ( ( z - 1 ) + v ) ) )
159 158 oveq2d 
 |-  ( x = z -> ( u + ( w x. ( ( x - 1 ) + v ) ) ) = ( u + ( w x. ( ( z - 1 ) + v ) ) ) )
160 159 fveq2d 
 |-  ( x = z -> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) = ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) )
161 160 mpteq2dv 
 |-  ( x = z -> ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) )
162 155 161 syl5eq 
 |-  ( x = z -> ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) = ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) )
163 162 cbvmptv 
 |-  ( x e. ( 1 ... v ) |-> ( y e. ( 1 ... w ) |-> ( h ` ( y + ( w x. ( ( x - 1 ) + v ) ) ) ) ) ) = ( z e. ( 1 ... v ) |-> ( u e. ( 1 ... w ) |-> ( h ` ( u + ( w x. ( ( z - 1 ) + v ) ) ) ) ) )
164 136 137 138 139 140 146 147 148 153 163 vdwlem9 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) /\ h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ) -> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) )
165 164 3expia 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> ( h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) -> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) )
166 165 ralrimiv 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) )
167 oveq2 
 |-  ( n = ( w x. ( 2 x. v ) ) -> ( 1 ... n ) = ( 1 ... ( w x. ( 2 x. v ) ) ) )
168 167 oveq2d 
 |-  ( n = ( w x. ( 2 x. v ) ) -> ( R ^m ( 1 ... n ) ) = ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) )
169 168 raleqdv 
 |-  ( n = ( w x. ( 2 x. v ) ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. f e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
170 breq2 
 |-  ( f = h -> ( <. ( m + 1 ) , K >. PolyAP f <-> <. ( m + 1 ) , K >. PolyAP h ) )
171 breq2 
 |-  ( f = h -> ( ( K + 1 ) MonoAP f <-> ( K + 1 ) MonoAP h ) )
172 170 171 orbi12d 
 |-  ( f = h -> ( ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) )
173 172 cbvralvw 
 |-  ( A. f e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) )
174 169 173 bitrdi 
 |-  ( n = ( w x. ( 2 x. v ) ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) <-> A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) )
175 174 rspcev 
 |-  ( ( ( w x. ( 2 x. v ) ) e. NN /\ A. h e. ( R ^m ( 1 ... ( w x. ( 2 x. v ) ) ) ) ( <. ( m + 1 ) , K >. PolyAP h \/ ( K + 1 ) MonoAP h ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
176 134 166 175 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
177 176 anassrs 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) /\ ( v e. NN /\ A. f e. ( ( R ^m ( 1 ... w ) ) ^m ( 1 ... v ) ) K MonoAP f ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
178 127 177 rexlimddv 
 |-  ( ( ( ph /\ m e. NN ) /\ ( w e. NN /\ A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
179 178 rexlimdvaa 
 |-  ( ( ph /\ m e. NN ) -> ( E. w e. NN A. g e. ( R ^m ( 1 ... w ) ) ( <. m , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
180 113 179 syl5bi 
 |-  ( ( ph /\ m e. NN ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
181 180 expcom 
 |-  ( m e. NN -> ( ph -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
182 181 a2d 
 |-  ( m e. NN -> ( ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. m , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) -> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( m + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) ) )
183 9 14 19 24 106 182 nnind 
 |-  ( M e. NN -> ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
184 4 183 mpcom 
 |-  ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )