Metamath Proof Explorer

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	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartel	$⊢ (φ \land I \in (0 \dots M)) \to P (I) \in [P (0), P (M)]$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3	1 2	iccpartf	$⊢ φ \to P : (0 \dots M) ⟶ [P (0), P (M)]$
4	3	ffvelrnda	$⊢ (φ \land I \in (0 \dots M)) \to P (I) \in [P (0), P (M)]$