Metamath Proof Explorer


Theorem iccpartimp

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

Ref Expression
Assertion iccpartimp M P RePart M I 0 ..^ M P * 0 M P I < P I + 1

Proof

Step Hyp Ref Expression
1 iccpart M P RePart M P * 0 M i 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 i 0 ..^ M P i < P i + 1 I 0 ..^ M P I < P I + 1
6 5 adantl P * 0 M i 0 ..^ M P i < P i + 1 I 0 ..^ M P I < P I + 1
7 simpl P * 0 M i 0 ..^ M P i < P i + 1 P * 0 M
8 6 7 jctild P * 0 M i 0 ..^ M P i < P i + 1 I 0 ..^ M P * 0 M P I < P I + 1
9 1 8 syl6bi M P RePart M I 0 ..^ M P * 0 M P I < P I + 1
10 9 3imp M P RePart M I 0 ..^ M P * 0 M P I < P I + 1