Metamath Proof Explorer

Theorem vdwlem1

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem1.r 
|- ( ph -> R e. Fin )
vdwlem1.k 
|- ( ph -> K e. NN )
vdwlem1.w 
|- ( ph -> W e. NN )
vdwlem1.f 
|- ( ph -> F : ( 1 ... W ) --> R )
vdwlem1.a 
|- ( ph -> A e. NN )
vdwlem1.m 
|- ( ph -> M e. NN )
vdwlem1.d 
|- ( ph -> D : ( 1 ... M ) --> NN )
vdwlem1.s 
|- ( ph -> A. i e. ( 1 ... M ) ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) C_ ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) )
vdwlem1.i 
|- ( ph -> I e. ( 1 ... M ) )
vdwlem1.e 
|- ( ph -> ( F ` A ) = ( F ` ( A + ( D ` I ) ) ) )
Assertion vdwlem1 
|- ( ph -> ( K + 1 ) MonoAP F )

Proof

Step Hyp Ref Expression
1 vdwlem1.r 
 |-  ( ph -> R e. Fin )
2 vdwlem1.k 
 |-  ( ph -> K e. NN )
3 vdwlem1.w 
 |-  ( ph -> W e. NN )
4 vdwlem1.f 
 |-  ( ph -> F : ( 1 ... W ) --> R )
5 vdwlem1.a 
 |-  ( ph -> A e. NN )
6 vdwlem1.m 
 |-  ( ph -> M e. NN )
7 vdwlem1.d 
 |-  ( ph -> D : ( 1 ... M ) --> NN )
8 vdwlem1.s 
 |-  ( ph -> A. i e. ( 1 ... M ) ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) C_ ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) )
9 vdwlem1.i 
 |-  ( ph -> I e. ( 1 ... M ) )
10 vdwlem1.e 
 |-  ( ph -> ( F ` A ) = ( F ` ( A + ( D ` I ) ) ) )
11 7 9 ffvelcdmd 
 |-  ( ph -> ( D ` I ) e. NN )
12 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
13 vdwapun 
 |-  ( ( K e. NN0 /\ A e. NN /\ ( D ` I ) e. NN ) -> ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) = ( { A } u. ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) ) )
14 12 5 11 13 syl3anc 
 |-  ( ph -> ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) = ( { A } u. ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) ) )
15 5 nnred 
 |-  ( ph -> A e. RR )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 6 16 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
18 eluzfz1 
 |-  ( M e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... M ) )
19 17 18 syl 
 |-  ( ph -> 1 e. ( 1 ... M ) )
20 7 19 ffvelcdmd 
 |-  ( ph -> ( D ` 1 ) e. NN )
21 5 20 nnaddcld 
 |-  ( ph -> ( A + ( D ` 1 ) ) e. NN )
22 21 nnred 
 |-  ( ph -> ( A + ( D ` 1 ) ) e. RR )
23 3 nnred 
 |-  ( ph -> W e. RR )
24 20 nnrpd 
 |-  ( ph -> ( D ` 1 ) e. RR+ )
25 15 24 ltaddrpd 
 |-  ( ph -> A < ( A + ( D ` 1 ) ) )
26 15 22 25 ltled 
 |-  ( ph -> A <_ ( A + ( D ` 1 ) ) )
27 fveq2 
 |-  ( i = 1 -> ( D ` i ) = ( D ` 1 ) )
28 27 oveq2d 
 |-  ( i = 1 -> ( A + ( D ` i ) ) = ( A + ( D ` 1 ) ) )
29 28 eleq1d 
 |-  ( i = 1 -> ( ( A + ( D ` i ) ) e. ( 1 ... W ) <-> ( A + ( D ` 1 ) ) e. ( 1 ... W ) ) )
30 8 r19.21bi 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) C_ ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) )
31 cnvimass 
 |-  ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) C_ dom F
32 31 4 fssdm 
 |-  ( ph -> ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) C_ ( 1 ... W ) )
33 32 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) C_ ( 1 ... W ) )
34 30 33 sstrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) C_ ( 1 ... W ) )
35 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
36 2 35 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
37 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
38 36 37 eleqtrdi 
 |-  ( ph -> ( K - 1 ) e. ( ZZ>= ` 0 ) )
39 eluzfz1 
 |-  ( ( K - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( K - 1 ) ) )
40 38 39 syl 
 |-  ( ph -> 0 e. ( 0 ... ( K - 1 ) ) )
41 40 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> 0 e. ( 0 ... ( K - 1 ) ) )
42 7 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( D ` i ) e. NN )
43 42 nncnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( D ` i ) e. CC )
44 43 mul02d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( 0 x. ( D ` i ) ) = 0 )
45 44 oveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( A + ( D ` i ) ) + ( 0 x. ( D ` i ) ) ) = ( ( A + ( D ` i ) ) + 0 ) )
46 5 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A e. NN )
47 46 42 nnaddcld 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( A + ( D ` i ) ) e. NN )
48 47 nncnd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( A + ( D ` i ) ) e. CC )
49 48 addridd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( A + ( D ` i ) ) + 0 ) = ( A + ( D ` i ) ) )
50 45 49 eqtr2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( 0 x. ( D ` i ) ) ) )
51 oveq1 
 |-  ( m = 0 -> ( m x. ( D ` i ) ) = ( 0 x. ( D ` i ) ) )
52 51 oveq2d 
 |-  ( m = 0 -> ( ( A + ( D ` i ) ) + ( m x. ( D ` i ) ) ) = ( ( A + ( D ` i ) ) + ( 0 x. ( D ` i ) ) ) )
53 52 rspceeqv 
 |-  ( ( 0 e. ( 0 ... ( K - 1 ) ) /\ ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( 0 x. ( D ` i ) ) ) ) -> E. m e. ( 0 ... ( K - 1 ) ) ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( m x. ( D ` i ) ) ) )
54 41 50 53 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> E. m e. ( 0 ... ( K - 1 ) ) ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( m x. ( D ` i ) ) ) )
55 2 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN )
56 55 nnnn0d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> K e. NN0 )
57 vdwapval 
 |-  ( ( K e. NN0 /\ ( A + ( D ` i ) ) e. NN /\ ( D ` i ) e. NN ) -> ( ( A + ( D ` i ) ) e. ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( m x. ( D ` i ) ) ) ) )
58 56 47 42 57 syl3anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( A + ( D ` i ) ) e. ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) <-> E. m e. ( 0 ... ( K - 1 ) ) ( A + ( D ` i ) ) = ( ( A + ( D ` i ) ) + ( m x. ( D ` i ) ) ) ) )
59 54 58 mpbird 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( A + ( D ` i ) ) e. ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) )
60 34 59 sseldd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( A + ( D ` i ) ) e. ( 1 ... W ) )
61 60 ralrimiva 
 |-  ( ph -> A. i e. ( 1 ... M ) ( A + ( D ` i ) ) e. ( 1 ... W ) )
62 29 61 19 rspcdva 
 |-  ( ph -> ( A + ( D ` 1 ) ) e. ( 1 ... W ) )
63 elfzle2 
 |-  ( ( A + ( D ` 1 ) ) e. ( 1 ... W ) -> ( A + ( D ` 1 ) ) <_ W )
64 62 63 syl 
 |-  ( ph -> ( A + ( D ` 1 ) ) <_ W )
65 15 22 23 26 64 letrd 
 |-  ( ph -> A <_ W )
66 5 16 eleqtrdi 
 |-  ( ph -> A e. ( ZZ>= ` 1 ) )
67 3 nnzd 
 |-  ( ph -> W e. ZZ )
68 elfz5 
 |-  ( ( A e. ( ZZ>= ` 1 ) /\ W e. ZZ ) -> ( A e. ( 1 ... W ) <-> A <_ W ) )
69 66 67 68 syl2anc 
 |-  ( ph -> ( A e. ( 1 ... W ) <-> A <_ W ) )
70 65 69 mpbird 
 |-  ( ph -> A e. ( 1 ... W ) )
71 eqidd 
 |-  ( ph -> ( F ` A ) = ( F ` A ) )
72 ffn 
 |-  ( F : ( 1 ... W ) --> R -> F Fn ( 1 ... W ) )
73 fniniseg 
 |-  ( F Fn ( 1 ... W ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> ( A e. ( 1 ... W ) /\ ( F ` A ) = ( F ` A ) ) ) )
74 4 72 73 3syl 
 |-  ( ph -> ( A e. ( `' F " { ( F ` A ) } ) <-> ( A e. ( 1 ... W ) /\ ( F ` A ) = ( F ` A ) ) ) )
75 70 71 74 mpbir2and 
 |-  ( ph -> A e. ( `' F " { ( F ` A ) } ) )
76 75 snssd 
 |-  ( ph -> { A } C_ ( `' F " { ( F ` A ) } ) )
77 fveq2 
 |-  ( i = I -> ( D ` i ) = ( D ` I ) )
78 77 oveq2d 
 |-  ( i = I -> ( A + ( D ` i ) ) = ( A + ( D ` I ) ) )
79 78 77 oveq12d 
 |-  ( i = I -> ( ( A + ( D ` i ) ) ( AP ` K ) ( D ` i ) ) = ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) )
80 78 fveq2d 
 |-  ( i = I -> ( F ` ( A + ( D ` i ) ) ) = ( F ` ( A + ( D ` I ) ) ) )
81 80 sneqd 
 |-  ( i = I -> { ( F ` ( A + ( D ` i ) ) ) } = { ( F ` ( A + ( D ` I ) ) ) } )
82 81 imaeq2d 
 |-  ( i = I -> ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) = ( `' F " { ( F ` ( A + ( D ` I ) ) ) } ) )
83 79 82 sseq12d 
 |-  ( i = I -> ( ( ( 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 ) ) ) } ) ) )
84 83 8 9 rspcdva 
 |-  ( ph -> ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) C_ ( `' F " { ( F ` ( A + ( D ` I ) ) ) } ) )
85 10 sneqd 
 |-  ( ph -> { ( F ` A ) } = { ( F ` ( A + ( D ` I ) ) ) } )
86 85 imaeq2d 
 |-  ( ph -> ( `' F " { ( F ` A ) } ) = ( `' F " { ( F ` ( A + ( D ` I ) ) ) } ) )
87 84 86 sseqtrrd 
 |-  ( ph -> ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) C_ ( `' F " { ( F ` A ) } ) )
88 76 87 unssd 
 |-  ( ph -> ( { A } u. ( ( A + ( D ` I ) ) ( AP ` K ) ( D ` I ) ) ) C_ ( `' F " { ( F ` A ) } ) )
89 14 88 eqsstrd 
 |-  ( ph -> ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) C_ ( `' F " { ( F ` A ) } ) )
90 oveq1 
 |-  ( a = A -> ( a ( AP ` ( K + 1 ) ) d ) = ( A ( AP ` ( K + 1 ) ) d ) )
91 90 sseq1d 
 |-  ( a = A -> ( ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) <-> ( A ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) ) )
92 oveq2 
 |-  ( d = ( D ` I ) -> ( A ( AP ` ( K + 1 ) ) d ) = ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) )
93 92 sseq1d 
 |-  ( d = ( D ` I ) -> ( ( A ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) <-> ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) C_ ( `' F " { ( F ` A ) } ) ) )
94 91 93 rspc2ev 
 |-  ( ( A e. NN /\ ( D ` I ) e. NN /\ ( A ( AP ` ( K + 1 ) ) ( D ` I ) ) C_ ( `' F " { ( F ` A ) } ) ) -> E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) )
95 5 11 89 94 syl3anc 
 |-  ( ph -> E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) )
96 fvex 
 |-  ( F ` A ) e. _V
97 sneq 
 |-  ( c = ( F ` A ) -> { c } = { ( F ` A ) } )
98 97 imaeq2d 
 |-  ( c = ( F ` A ) -> ( `' F " { c } ) = ( `' F " { ( F ` A ) } ) )
99 98 sseq2d 
 |-  ( c = ( F ` A ) -> ( ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { c } ) <-> ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) ) )
100 99 2rexbidv 
 |-  ( c = ( F ` A ) -> ( E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { c } ) <-> E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) ) )
101 96 100 spcev 
 |-  ( E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { ( F ` A ) } ) -> E. c E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { c } ) )
102 95 101 syl 
 |-  ( ph -> E. c E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { c } ) )
103 ovex 
 |-  ( 1 ... W ) e. _V
104 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
105 12 104 syl 
 |-  ( ph -> ( K + 1 ) e. NN0 )
106 103 105 4 vdwmc 
 |-  ( ph -> ( ( K + 1 ) MonoAP F <-> E. c E. a e. NN E. d e. NN ( a ( AP ` ( K + 1 ) ) d ) C_ ( `' F " { c } ) ) )
107 102 106 mpbird 
 |-  ( ph -> ( K + 1 ) MonoAP F )