Theorem iccpartel

Description: If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	|- ( ph -> M e. NN )
	iccpartgtprec.p	|- ( ph -> P e. ( RePart ` M ) )
Assertion	iccpartel	|- ( ( ph /\ I e. ( 0 ... M ) ) -> ( P ` I ) e. ( ( P ` 0 ) [,] ( P ` M ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	|- ( ph -> M e. NN )
2		iccpartgtprec.p	|- ( ph -> P e. ( RePart ` M ) )
3	1 2	iccpartf	|- ( ph -> P : ( 0 ... M ) --> ( ( P ` 0 ) [,] ( P ` M ) ) )
4	3	ffvelrnda	|- ( ( ph /\ I e. ( 0 ... M ) ) -> ( P ` I ) e. ( ( P ` 0 ) [,] ( P ` M ) ) )