Metamath Proof Explorer

Theorem vdwlem11

Description: Lemma for vdw . (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 )
Assertion vdwlem11 
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( 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 hashcl 
 |-  ( R e. Fin -> ( # ` R ) e. NN0 )
5 1 4 syl 
 |-  ( ph -> ( # ` R ) e. NN0 )
6 nn0p1nn 
 |-  ( ( # ` R ) e. NN0 -> ( ( # ` R ) + 1 ) e. NN )
7 5 6 syl 
 |-  ( ph -> ( ( # ` R ) + 1 ) e. NN )
8 1 2 3 7 vdwlem10 
 |-  ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
9 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> R e. Fin )
10 ovex 
 |-  ( 1 ... n ) e. _V
11 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... n ) e. _V ) -> ( f e. ( R ^m ( 1 ... n ) ) <-> f : ( 1 ... n ) --> R ) )
12 9 10 11 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( f e. ( R ^m ( 1 ... n ) ) <-> f : ( 1 ... n ) --> R ) )
13 12 biimpa 
 |-  ( ( ( ph /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> f : ( 1 ... n ) --> R )
14 5 nn0red 
 |-  ( ph -> ( # ` R ) e. RR )
15 14 ltp1d 
 |-  ( ph -> ( # ` R ) < ( ( # ` R ) + 1 ) )
16 peano2re 
 |-  ( ( # ` R ) e. RR -> ( ( # ` R ) + 1 ) e. RR )
17 14 16 syl 
 |-  ( ph -> ( ( # ` R ) + 1 ) e. RR )
18 14 17 ltnled 
 |-  ( ph -> ( ( # ` R ) < ( ( # ` R ) + 1 ) <-> -. ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
19 15 18 mpbid 
 |-  ( ph -> -. ( ( # ` R ) + 1 ) <_ ( # ` R ) )
20 19 adantr 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> -. ( ( # ` R ) + 1 ) <_ ( # ` R ) )
21 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
22 2 21 syl 
 |-  ( ph -> K e. NN )
23 22 adantr 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> K e. NN )
24 23 nnnn0d 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> K e. NN0 )
25 simprr 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> f : ( 1 ... n ) --> R )
26 7 adantr 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> ( ( # ` R ) + 1 ) e. NN )
27 eqid 
 |-  ( 1 ... ( ( # ` R ) + 1 ) ) = ( 1 ... ( ( # ` R ) + 1 ) )
28 10 24 25 26 27 vdwpc 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f <-> E. a e. NN E. d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ( A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( ( # ` R ) + 1 ) ) ) )
29 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> R e. Fin )
30 25 ad2antrr 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> f : ( 1 ... n ) --> R )
31 25 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> f : ( 1 ... n ) --> R )
32 simpr 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) )
33 cnvimass 
 |-  ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) C_ dom f
34 32 33 sstrdi 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ dom f )
35 31 34 fssdmd 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( 1 ... n ) )
36 22 ad3antrrr 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> K e. NN )
37 simplrl 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> a e. NN )
38 simprr 
 |-  ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) -> d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) )
39 nnex 
 |-  NN e. _V
40 ovex 
 |-  ( 1 ... ( ( # ` R ) + 1 ) ) e. _V
41 39 40 elmap 
 |-  ( d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) <-> d : ( 1 ... ( ( # ` R ) + 1 ) ) --> NN )
42 38 41 sylib 
 |-  ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) -> d : ( 1 ... ( ( # ` R ) + 1 ) ) --> NN )
43 42 ffvelrnda 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> ( d ` i ) e. NN )
44 37 43 nnaddcld 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> ( a + ( d ` i ) ) e. NN )
45 vdwapid1 
 |-  ( ( K e. NN /\ ( a + ( d ` i ) ) e. NN /\ ( d ` i ) e. NN ) -> ( a + ( d ` i ) ) e. ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) )
46 36 44 43 45 syl3anc 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> ( a + ( d ` i ) ) e. ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) )
47 46 adantr 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( a + ( d ` i ) ) e. ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) )
48 35 47 sseldd 
 |-  ( ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) /\ ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( a + ( d ` i ) ) e. ( 1 ... n ) )
49 48 ex 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> ( ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) -> ( a + ( d ` i ) ) e. ( 1 ... n ) ) )
50 ffvelrn 
 |-  ( ( f : ( 1 ... n ) --> R /\ ( a + ( d ` i ) ) e. ( 1 ... n ) ) -> ( f ` ( a + ( d ` i ) ) ) e. R )
51 30 49 50 syl6an 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ i e. ( 1 ... ( ( # ` R ) + 1 ) ) ) -> ( ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) -> ( f ` ( a + ( d ` i ) ) ) e. R ) )
52 51 ralimdva 
 |-  ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) -> ( A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) -> A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( f ` ( a + ( d ` i ) ) ) e. R ) )
53 52 imp 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( f ` ( a + ( d ` i ) ) ) e. R )
54 eqid 
 |-  ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) = ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) )
55 54 fmpt 
 |-  ( A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( f ` ( a + ( d ` i ) ) ) e. R <-> ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )
56 53 55 sylib 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )
57 56 frnd 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) C_ R )
58 ssdomg 
 |-  ( R e. Fin -> ( ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) C_ R -> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ~<_ R ) )
59 29 57 58 sylc 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ~<_ R )
60 29 57 ssfid 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) e. Fin )
61 hashdom 
 |-  ( ( ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) e. Fin /\ R e. Fin ) -> ( ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) <_ ( # ` R ) <-> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ~<_ R ) )
62 60 29 61 syl2anc 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) <_ ( # ` R ) <-> ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ~<_ R ) )
63 59 62 mpbird 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) <_ ( # ` R ) )
64 breq1 
 |-  ( ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( ( # ` R ) + 1 ) -> ( ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) <_ ( # ` R ) <-> ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
65 63 64 syl5ibcom 
 |-  ( ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) /\ A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) ) -> ( ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( ( # ` R ) + 1 ) -> ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
66 65 expimpd 
 |-  ( ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) /\ ( a e. NN /\ d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ) ) -> ( ( A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( ( # ` R ) + 1 ) ) -> ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
67 66 rexlimdvva 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> ( E. a e. NN E. d e. ( NN ^m ( 1 ... ( ( # ` R ) + 1 ) ) ) ( A. i e. ( 1 ... ( ( # ` R ) + 1 ) ) ( ( a + ( d ` i ) ) ( AP ` K ) ( d ` i ) ) C_ ( `' f " { ( f ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... ( ( # ` R ) + 1 ) ) |-> ( f ` ( a + ( d ` i ) ) ) ) ) = ( ( # ` R ) + 1 ) ) -> ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
68 28 67 sylbid 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f -> ( ( # ` R ) + 1 ) <_ ( # ` R ) ) )
69 20 68 mtod 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> -. <. ( ( # ` R ) + 1 ) , K >. PolyAP f )
70 biorf 
 |-  ( -. <. ( ( # ` R ) + 1 ) , K >. PolyAP f -> ( ( K + 1 ) MonoAP f <-> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
71 69 70 syl 
 |-  ( ( ph /\ ( n e. NN /\ f : ( 1 ... n ) --> R ) ) -> ( ( K + 1 ) MonoAP f <-> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
72 71 anassrs 
 |-  ( ( ( ph /\ n e. NN ) /\ f : ( 1 ... n ) --> R ) -> ( ( K + 1 ) MonoAP f <-> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
73 13 72 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> ( ( K + 1 ) MonoAP f <-> ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
74 73 ralbidva 
 |-  ( ( ph /\ n e. NN ) -> ( A. f e. ( R ^m ( 1 ... n ) ) ( K + 1 ) MonoAP f <-> A. f e. ( R ^m ( 1 ... n ) ) ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
75 74 rexbidva 
 |-  ( ph -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( K + 1 ) MonoAP f <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. ( ( # ` R ) + 1 ) , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) ) )
76 8 75 mpbird 
 |-  ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( K + 1 ) MonoAP f )