Step |
Hyp |
Ref |
Expression |
1 |
|
iccpart |
|- ( M e. NN -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) ) |
2 |
|
fveq2 |
|- ( i = I -> ( P ` i ) = ( P ` I ) ) |
3 |
|
fvoveq1 |
|- ( i = I -> ( P ` ( i + 1 ) ) = ( P ` ( I + 1 ) ) ) |
4 |
2 3
|
breq12d |
|- ( i = I -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( P ` I ) < ( P ` ( I + 1 ) ) ) ) |
5 |
4
|
rspccv |
|- ( A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) -> ( I e. ( 0 ..^ M ) -> ( P ` I ) < ( P ` ( I + 1 ) ) ) ) |
6 |
5
|
adantl |
|- ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> ( I e. ( 0 ..^ M ) -> ( P ` I ) < ( P ` ( I + 1 ) ) ) ) |
7 |
|
simpl |
|- ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> P e. ( RR* ^m ( 0 ... M ) ) ) |
8 |
6 7
|
jctild |
|- ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> ( I e. ( 0 ..^ M ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) ) ) |
9 |
1 8
|
syl6bi |
|- ( M e. NN -> ( P e. ( RePart ` M ) -> ( I e. ( 0 ..^ M ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) ) ) ) |
10 |
9
|
3imp |
|- ( ( M e. NN /\ P e. ( RePart ` M ) /\ I e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) ) |