Metamath Proof Explorer

Theorem iccpartimp

Description: Implications for a class being a partition. (Contributed by AV, 11-Jul-2020)

Ref Expression
Assertion iccpartimp 
|- ( ( M e. NN /\ P e. ( RePart ` M ) /\ I e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) )

Proof

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 biimtrdi 
 |-  ( 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 ) ) ) )