df-iccp

Description: Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020)

		Ref	Expression
	Assertion	df-iccp	$⊢ RePart = (m \in ℕ ⟼ \{p \in ({ℝ^{*}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciccp	$class RePart$
1		vm	$setvar m$
2		cn	$class ℕ$
3		vp	$setvar p$
4		cxr	$class ℝ^{*}$
5		cmap	$class ↑_{𝑚}$
6		cc0	$class 0$
7		cfz	$class \dots$
8	1	cv	$setvar m$
9	6 8 7	co	$class (0 \dots m)$
10	4 9 5	co	$class ({ℝ^{*}}^{(0 \dots m)})$
11		vi	$setvar i$
12		cfzo	$class ..^$
13	6 8 12	co	$class (0 ..^m)$
14	3	cv	$setvar p$
15	11	cv	$setvar i$
16	15 14	cfv	$class p (i)$
17		clt	$class <$
18		caddc	$class +$
19		c1	$class 1$
20	15 19 18	co	$class (i + 1)$
21	20 14	cfv	$class p (i + 1)$
22	16 21 17	wbr	$wff p (i) < p (i + 1)$
23	22 11 13	wral	$wff \forall i \in (0 ..^m) p (i) < p (i + 1)$
24	23 3 10	crab	$class \{p \in ({ℝ^{*}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\}$
25	1 2 24	cmpt	$class (m \in ℕ ⟼ \{p \in ({ℝ^{*}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\})$
26	0 25	wceq	$wff RePart = (m \in ℕ ⟼ \{p \in ({ℝ^{*}}^{(0 \dots m)}) \| \forall i \in (0 ..^m) p (i) < p (i + 1)\})$

Metamath Proof Explorer

Definition df-iccp

Detailed syntax breakdown