Metamath Proof Explorer

Theorem iccpart

Description: A special partition. Corresponds to fourierdlem2 in GS's mathbox. (Contributed by AV, 9-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 iccpval 
 |-  ( M e. NN -> ( RePart ` M ) = { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
2 1 eleq2d 
 |-  ( M e. NN -> ( P e. ( RePart ` M ) <-> P e. { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } ) )
3 fveq1 
 |-  ( p = P -> ( p ` i ) = ( P ` i ) )
4 fveq1 
 |-  ( p = P -> ( p ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
5 3 4 breq12d 
 |-  ( p = P -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( P ` i ) < ( P ` ( i + 1 ) ) ) )
6 5 ralbidv 
 |-  ( p = P -> ( A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
7 6 elrab 
 |-  ( P e. { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
8 2 7 bitrdi 
 |-  ( M e. NN -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )