iccpartres

Description: The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020)

		Ref	Expression
	Assertion	iccpartres	$⊢ (M \in ℕ \land P \in RePart (M + 1)) \to {P ↾}_{(0 \dots M)} \in RePart (M)$

Proof

Step	Hyp	Ref	Expression
1		peano2nn	$⊢ M \in ℕ \to M + 1 \in ℕ$
2		iccpart	$⊢ M + 1 \in ℕ \to (P \in RePart (M + 1) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)))$
3	1 2	syl	$⊢ M \in ℕ \to (P \in RePart (M + 1) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)))$
4		simpl	$⊢ (P \in ({ℝ^{}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)) \to P \in ({ℝ^{}}^{(0 \dots M + 1)})$
5		nnz	$⊢ M \in ℕ \to M \in ℤ$
6		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
7	5 6	syl	$⊢ M \in ℕ \to M \in ℤ_{\geq M}$
8		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
9	7 8	syl	$⊢ M \in ℕ \to M + 1 \in ℤ_{\geq M}$
10		fzss2	$⊢ M + 1 \in ℤ_{\geq M} \to (0 \dots M) \subseteq (0 \dots M + 1)$
11	9 10	syl	$⊢ M \in ℕ \to (0 \dots M) \subseteq (0 \dots M + 1)$
12		elmapssres	$⊢ (P \in ({ℝ^{}}^{(0 \dots M + 1)}) \land (0 \dots M) \subseteq (0 \dots M + 1)) \to {P ↾}_{(0 \dots M)} \in ({ℝ^{}}^{(0 \dots M)})$
13	4 11 12	syl2anr	$⊢ (M \in ℕ \land (P \in ({ℝ^{}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to {P ↾}_{(0 \dots M)} \in ({ℝ^{}}^{(0 \dots M)})$
14		fzoss2	$⊢ M + 1 \in ℤ_{\geq M} \to (0 ..^M) \subseteq (0 ..^M + 1)$
15	9 14	syl	$⊢ M \in ℕ \to (0 ..^M) \subseteq (0 ..^M + 1)$
16		ssralv	$⊢ (0 ..^M) \subseteq (0 ..^M + 1) \to (\forall i \in (0 ..^M + 1) P (i) < P (i + 1) \to \forall i \in (0 ..^M) P (i) < P (i + 1))$
17	15 16	syl	$⊢ M \in ℕ \to (\forall i \in (0 ..^M + 1) P (i) < P (i + 1) \to \forall i \in (0 ..^M) P (i) < P (i + 1))$
18	17	adantld	$⊢ M \in ℕ \to ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)) \to \forall i \in (0 ..^M) P (i) < P (i + 1))$
19	18	imp	$⊢ (M \in ℕ \land (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to \forall i \in (0 ..^M) P (i) < P (i + 1)$
20		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
21	20	a1i	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \to (0 ..^M) \subseteq (0 \dots M)$
22	21	sselda	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to i \in (0 \dots M)$
23		fvres	$⊢ i \in (0 \dots M) \to ({P ↾}_{(0 \dots M)}) (i) = P (i)$
24	23	eqcomd	$⊢ i \in (0 \dots M) \to P (i) = ({P ↾}_{(0 \dots M)}) (i)$
25	22 24	syl	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to P (i) = ({P ↾}_{(0 \dots M)}) (i)$
26		simpr	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to i \in (0 ..^M)$
27		elfzouz	$⊢ i \in (0 ..^M) \to i \in ℤ_{\geq 0}$
28	27	adantl	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to i \in ℤ_{\geq 0}$
29		fzofzp1b	$⊢ i \in ℤ_{\geq 0} \to (i \in (0 ..^M) \leftrightarrow i + 1 \in (0 \dots M))$
30	28 29	syl	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to (i \in (0 ..^M) \leftrightarrow i + 1 \in (0 \dots M))$
31	26 30	mpbid	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
32		fvres	$⊢ i + 1 \in (0 \dots M) \to ({P ↾}_{(0 \dots M)}) (i + 1) = P (i + 1)$
33	31 32	syl	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to ({P ↾}_{(0 \dots M)}) (i + 1) = P (i + 1)$
34	33	eqcomd	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to P (i + 1) = ({P ↾}_{(0 \dots M)}) (i + 1)$
35	25 34	breq12d	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to (P (i) < P (i + 1) \leftrightarrow ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1))$
36	35	biimpd	$⊢ ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \land i \in (0 ..^M)) \to (P (i) < P (i + 1) \to ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1))$
37	36	ralimdva	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land M \in ℕ) \to (\forall i \in (0 ..^M) P (i) < P (i + 1) \to \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1))$
38	37	ex	$⊢ P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \to (M \in ℕ \to (\forall i \in (0 ..^M) P (i) < P (i + 1) \to \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1)))$
39	38	adantr	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)) \to (M \in ℕ \to (\forall i \in (0 ..^M) P (i) < P (i + 1) \to \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1)))$
40	39	impcom	$⊢ (M \in ℕ \land (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to (\forall i \in (0 ..^M) P (i) < P (i + 1) \to \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1))$
41	19 40	mpd	$⊢ (M \in ℕ \land (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1)$
42		iccpart	$⊢ M \in ℕ \to ({P ↾}_{(0 \dots M)} \in RePart (M) \leftrightarrow ({P ↾}_{(0 \dots M)} \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1)))$
43	42	adantr	$⊢ (M \in ℕ \land (P \in ({ℝ^{}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to ({P ↾}_{(0 \dots M)} \in RePart (M) \leftrightarrow ({P ↾}_{(0 \dots M)} \in ({ℝ^{}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) ({P ↾}_{(0 \dots M)}) (i) < ({P ↾}_{(0 \dots M)}) (i + 1)))$
44	13 41 43	mpbir2and	$⊢ (M \in ℕ \land (P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1))) \to {P ↾}_{(0 \dots M)} \in RePart (M)$
45	44	ex	$⊢ M \in ℕ \to ((P \in ({ℝ^{*}}^{(0 \dots M + 1)}) \land \forall i \in (0 ..^M + 1) P (i) < P (i + 1)) \to {P ↾}_{(0 \dots M)} \in RePart (M))$
46	3 45	sylbid	$⊢ M \in ℕ \to (P \in RePart (M + 1) \to {P ↾}_{(0 \dots M)} \in RePart (M))$
47	46	imp	$⊢ (M \in ℕ \land P \in RePart (M + 1)) \to {P ↾}_{(0 \dots M)} \in RePart (M)$

Metamath Proof Explorer

Theorem iccpartres

Proof