Metamath Proof Explorer


Theorem iccpartimp

Description: Implications for a class being a partition. (Contributed by AV, 11-Jul-2020)

Ref Expression
Assertion iccpartimp ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpart ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
2 fveq2 ( 𝑖 = 𝐼 → ( 𝑃𝑖 ) = ( 𝑃𝐼 ) )
3 fvoveq1 ( 𝑖 = 𝐼 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
4 2 3 breq12d ( 𝑖 = 𝐼 → ( ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
5 4 rspccv ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
6 5 adantl ( ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
7 simpl ( ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) )
8 6 7 jctild ( ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
9 1 8 syl6bi ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) )
10 9 3imp ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )