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 = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )

Distinct variable group:   i, m, p

Detailed syntax breakdown of Definition df-iccp

Step	Hyp	Ref	Expression
1		ciccp 41349	. 2 class RePart
2		vm	. . 3 setvar m
3		cn 11020	. . 3 class NN
4		vi	. . . . . . . 8 setvar i
5	4	cv 1482	. . . . . . 7 class i
6		vp	. . . . . . . 8 setvar p
7	6	cv 1482	. . . . . . 7 class p
8	5, 7	cfv 5888	. . . . . 6 class ( p ` i )
9		c1 9937	. . . . . . . 8 class 1
10		caddc 9939	. . . . . . . 8 class +
11	5, 9, 10	co 6650	. . . . . . 7 class ( i + 1 )
12	11, 7	cfv 5888	. . . . . 6 class ( p ` ( i + 1 ) )
13		clt 10074	. . . . . 6 class <
14	8, 12, 13	wbr 4653	. . . . 5 wff ( p ` i ) < ( p ` ( i + 1 ) )
15		cc0 9936	. . . . . 6 class 0
16	2	cv 1482	. . . . . 6 class m
17		cfzo 12465	. . . . . 6 class ..^
18	15, 16, 17	co 6650	. . . . 5 class ( 0..^ m )
19	14, 4, 18	wral 2912	. . . 4 wff A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) )
20		cxr 10073	. . . . 5 class RR*
21		cfz 12326	. . . . . 6 class ...
22	15, 16, 21	co 6650	. . . . 5 class ( 0 ... m )
23		cmap 7857	. . . . 5 class ^m
24	20, 22, 23	co 6650	. . . 4 class ( RR* ^m ( 0 ... m ) )
25	19, 6, 24	crab 2916	. . 3 class { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) }
26	2, 3, 25	cmpt 4729	. 2 class ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
27	1, 26	wceq 1483	1 wff RePart = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )

This definition is referenced by:  iccpval  41351