Definition df-iccp 41350

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.)

Assertion

Ref	Expression
df-iccp	⊢ RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})

Distinct variable group:   𝑖,𝑚,𝑝

Detailed syntax breakdown of Definition df-iccp

Step	Hyp	Ref	Expression
1		ciccp 41349	. 2 class RePart
2		vm	. . 3 setvar 𝑚
3		cn 11020	. . 3 class ℕ
4		vi	. . . . . . . 8 setvar 𝑖
5	4	cv 1482	. . . . . . 7 class 𝑖
6		vp	. . . . . . . 8 setvar 𝑝
7	6	cv 1482	. . . . . . 7 class 𝑝
8	5, 7	cfv 5888	. . . . . 6 class (𝑝‘𝑖)
9		c1 9937	. . . . . . . 8 class 1
10		caddc 9939	. . . . . . . 8 class +
11	5, 9, 10	co 6650	. . . . . . 7 class (𝑖 + 1)
12	11, 7	cfv 5888	. . . . . 6 class (𝑝‘(𝑖 + 1))
13		clt 10074	. . . . . 6 class <
14	8, 12, 13	wbr 4653	. . . . 5 wff (𝑝‘𝑖) < (𝑝‘(𝑖 + 1))
15		cc0 9936	. . . . . 6 class 0
16	2	cv 1482	. . . . . 6 class 𝑚
17		cfzo 12465	. . . . . 6 class ..^
18	15, 16, 17	co 6650	. . . . 5 class (0..^𝑚)
19	14, 4, 18	wral 2912	. . . 4 wff ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))
20		cxr 10073	. . . . 5 class ℝ*
21		cfz 12326	. . . . . 6 class ...
22	15, 16, 21	co 6650	. . . . 5 class (0...𝑚)
23		cmap 7857	. . . . 5 class ↑𝑚
24	20, 22, 23	co 6650	. . . 4 class (ℝ* ↑𝑚 (0...𝑚))
25	19, 6, 24	crab 2916	. . 3 class {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}
26	2, 3, 25	cmpt 4729	. 2 class (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})
27	1, 26	wceq 1483	1 wff RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑𝑚 (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})

This definition is referenced by:  iccpval  41351