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	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion	iccpartel	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝐼 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3	1 2	iccpartf	⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )
4	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝐼 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )