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 MRePartM=p*0M|i0..^Mpi<pi+1

Proof

Step Hyp Ref Expression
1 oveq2 m=M0m=0M
2 1 oveq2d m=M*0m=*0M
3 oveq2 m=M0..^m=0..^M
4 3 raleqdv m=Mi0..^mpi<pi+1i0..^Mpi<pi+1
5 2 4 rabeqbidv m=Mp*0m|i0..^mpi<pi+1=p*0M|i0..^Mpi<pi+1
6 df-iccp RePart=mp*0m|i0..^mpi<pi+1
7 ovex *0MV
8 7 rabex p*0M|i0..^Mpi<pi+1V
9 5 6 8 fvmpt MRePartM=p*0M|i0..^Mpi<pi+1