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 RePart M = p * 0 M | i 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 * 0 m = * 0 M
3 oveq2 m = M 0 ..^ m = 0 ..^ M
4 3 raleqdv m = M i 0 ..^ m p i < p i + 1 i 0 ..^ M p i < p i + 1
5 2 4 rabeqbidv m = M p * 0 m | i 0 ..^ m p i < p i + 1 = p * 0 M | i 0 ..^ M p i < p i + 1
6 df-iccp RePart = m p * 0 m | i 0 ..^ m p i < p i + 1
7 ovex * 0 M V
8 7 rabex p * 0 M | i 0 ..^ M p i < p i + 1 V
9 5 6 8 fvmpt M RePart M = p * 0 M | i 0 ..^ M p i < p i + 1