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

Metamath Proof Explorer

Theorem iccpval

Description: Partition consisting of a fixed number M of parts. (Contributed by AV, 9-Jul-2020)

Ref Expression
Assertion iccpval ( 𝑀 ∈ ℕ → ( RePart ‘ 𝑀 ) = { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 0 ... 𝑚 ) = ( 0 ... 𝑀 ) )
2 1 oveq2d ⊢ ( 𝑚 = 𝑀 → ( ℝ* ↑m ( 0 ... 𝑚 ) ) = ( ℝ* ↑m ( 0 ... 𝑀 ) ) )
3 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 0 ..^ 𝑚 ) = ( 0 ..^ 𝑀 ) )
4 3 raleqdv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
5 2 4 rabeqbidv ⊢ ( 𝑚 = 𝑀 → { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } = { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )
6 df-iccp ⊢ RePart = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑚 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )
7 ovex ⊢ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∈ V
8 7 rabex ⊢ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ∈ V
9 5 6 8 fvmpt ⊢ ( 𝑀 ∈ ℕ → ( RePart ‘ 𝑀 ) = { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )