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 
|- ( ph -> R e. Fin )
vdw.k 
|- ( ph -> K e. NN0 )
Assertion vdwlem13 
|- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f )

Proof

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