This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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