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	$$⊢\phi \to M\in \mathbb{N}$$
	iccpartgtprec.p	$$⊢\phi \to P\in \mathrm{RePart}\left(M\right)$$
Assertion	iccpartel	$$⊢\left(\phi \wedge I\in \left(0\dots M\right)\right)\to P\left(I\right)\in \left[P\left(0\right),P\left(M\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$$⊢\phi \to M\in \mathbb{N}$$
2		iccpartgtprec.p	$$⊢\phi \to P\in \mathrm{RePart}\left(M\right)$$
3	1 2	iccpartf	$$⊢\phi \to P:\left(0\dots M\right)⟶\left[P\left(0\right),P\left(M\right)\right]$$
4	3	ffvelcdmda	$$⊢\left(\phi \wedge I\in \left(0\dots M\right)\right)\to P\left(I\right)\in \left[P\left(0\right),P\left(M\right)\right]$$