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