iccpval

Description: Partition consisting of a fixed number M of parts. (Contributed by AV, 9-Jul-2020)

		Ref	Expression
	Assertion	iccpval	$⊢ M \in ℕ \to RePart (M) = \{p \in ({ℝ^{*}}^{(0 \dots M)}) \| \forall i \in (0 ..^M) p (i) < p (i + 1)\}$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ m = M \to (0 \dots m) = (0 \dots M)$
2	1	oveq2d	$⊢ m = M \to {ℝ^{}}^{(0 \dots m)} = {ℝ^{}}^{(0 \dots M)}$
3		oveq2	$⊢ m = M \to (0 ..^m) = (0 ..^M)$
4	3	raleqdv	$⊢ m = M \to (\forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall i \in (0 ..^M) p (i) < p (i + 1))$
5	2 4	rabeqbidv	$⊢ m = M \to \{p \in ({ℝ^{}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\} = \{p \in ({ℝ^{}}^{(0 \dots M)}) \| \forall i \in (0 ..^M) p (i) < p (i + 1)\}$
6		df-iccp	$⊢ RePart = (m \in ℕ ⟼ \{p \in ({ℝ^{*}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\})$
7		ovex	$⊢ {ℝ^{*}}^{(0 \dots M)} \in V$
8	7	rabex	$⊢ \{p \in ({ℝ^{*}}^{(0 \dots M)}) \| \forall i \in (0 ..^M) p (i) < p (i + 1)\} \in V$
9	5 6 8	fvmpt	$⊢ M \in ℕ \to RePart (M) = \{p \in ({ℝ^{*}}^{(0 \dots M)}) \| \forall i \in (0 ..^M) p (i) < p (i + 1)\}$

Metamath Proof Explorer