Definition 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 ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciccp	⊢ RePart
1		vm	⊢ 𝑚
2		cn	⊢ ℕ
3		vp	⊢ 𝑝
4		cxr	⊢ ℝ*
5		cmap	⊢ ↑m
6		cc0	⊢ 0
7		cfz	⊢ ...
8	1	cv	⊢ 𝑚
9	6 8 7	co	⊢ ( 0 ... 𝑚 )
10	4 9 5	co	⊢ ( ℝ* ↑m ( 0 ... 𝑚 ) )
11		vi	⊢ 𝑖
12		cfzo	⊢ ..^
13	6 8 12	co	⊢ ( 0 ..^ 𝑚 )
14	3	cv	⊢ 𝑝
15	11	cv	⊢ 𝑖
16	15 14	cfv	⊢ ( 𝑝 ‘ 𝑖 )
17		clt	⊢ <
18		caddc	⊢ +
19		c1	⊢ 1
20	15 19 18	co	⊢ ( 𝑖 + 1 )
21	20 14	cfv	⊢ ( 𝑝 ‘ ( 𝑖 + 1 ) )
22	16 21 17	wbr	⊢ ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) )
23	22 11 13	wral	⊢ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) )
24	23 3 10	crab	⊢ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) }
25	1 2 24	cmpt	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )
26	0 25	wceq	⊢ RePart = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )