Metamath Proof Explorer

Theorem iccpval

Description: Partition consisting of a fixed number M of parts. (Contributed by AV, 9-Jul-2020)

Ref Expression
Assertion iccpval 
|- ( M e. NN -> ( RePart ` M ) = { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = M -> ( 0 ... m ) = ( 0 ... M ) )
2 1 oveq2d 
 |-  ( m = M -> ( RR* ^m ( 0 ... m ) ) = ( RR* ^m ( 0 ... M ) ) )
3 oveq2 
 |-  ( m = M -> ( 0 ..^ m ) = ( 0 ..^ M ) )
4 3 raleqdv 
 |-  ( m = M -> ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) )
5 2 4 rabeqbidv 
 |-  ( m = M -> { 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 ) ) } )
6 df-iccp 
 |-  RePart = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
7 ovex 
 |-  ( RR* ^m ( 0 ... M ) ) e. _V
8 7 rabex 
 |-  { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } e. _V
9 5 6 8 fvmpt 
 |-  ( M e. NN -> ( RePart ` M ) = { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } )