iccpartimp

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

		Ref	Expression
	Assertion	iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land I \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I) < P (I + 1))$

Step	Hyp	Ref	Expression
1		iccpart	$⊢ M \in ℕ \to (P \in RePart (M) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)))$
2		fveq2	$⊢ i = I \to P (i) = P (I)$
3		fvoveq1	$⊢ i = I \to P (i + 1) = P (I + 1)$
4	2 3	breq12d	$⊢ i = I \to (P (i) < P (i + 1) \leftrightarrow P (I) < P (I + 1))$
5	4	rspccv	$⊢ \forall i \in (0 ..^M) P (i) < P (i + 1) \to (I \in (0 ..^M) \to P (I) < P (I + 1))$
6	5	adantl	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to (I \in (0 ..^M) \to P (I) < P (I + 1))$
7		simpl	$⊢ (P \in ({ℝ^{}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to P \in ({ℝ^{}}^{(0 \dots M)})$
8	6 7	jctild	$⊢ (P \in ({ℝ^{}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to (I \in (0 ..^M) \to (P \in ({ℝ^{}}^{(0 \dots M)}) \land P (I) < P (I + 1)))$
9	1 8	syl6bi	$⊢ M \in ℕ \to (P \in RePart (M) \to (I \in (0 ..^M) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I) < P (I + 1))))$
10	9	3imp	$⊢ (M \in ℕ \land P \in RePart (M) \land I \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I) < P (I + 1))$

Metamath Proof Explorer