Metamath Proof Explorer

Theorem iccpartimp

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

Ref Expression
Assertion iccpartimp ⊢ M ∈ ℕ ∧ P ∈ RePart ⁡ M ∧ I ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I < P ⁡ I + 1

Proof

Step Hyp Ref Expression
1 iccpart ⊢ M ∈ ℕ → P ∈ RePart ⁡ M ↔ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1
2 fveq2 ⊢ i = I → P ⁡ i = P ⁡ I
3 fvoveq1 ⊢ i = I → P ⁡ i + 1 = P ⁡ I + 1
4 2 3 breq12d ⊢ i = I → P ⁡ i < P ⁡ i + 1 ↔ P ⁡ I < P ⁡ I + 1
5 4 rspccv ⊢ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1 → I ∈ 0 ..^ M → P ⁡ I < P ⁡ I + 1
6 5 adantl ⊢ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1 → I ∈ 0 ..^ M → P ⁡ I < P ⁡ I + 1
7 simpl ⊢ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1 → P ∈ ℝ * 0 … M
8 6 7 jctild ⊢ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1 → I ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I < P ⁡ I + 1
9 1 8 biimtrdi ⊢ M ∈ ℕ → P ∈ RePart ⁡ M → I ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I < P ⁡ I + 1
10 9 3imp ⊢ M ∈ ℕ ∧ P ∈ RePart ⁡ M ∧ I ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I < P ⁡ I + 1