Metamath Proof Explorer

Theorem iccpartf

Description: The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 14-Jul-2020)

		Ref	Expression
	Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
	Assertion	iccpartf	$⊢ φ \to P : (0 \dots M) ⟶ [P (0), P (M)]$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		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)))$
4		elmapfn	$⊢ P \in ({ℝ^{*}}^{(0 \dots M)}) \to P Fn (0 \dots M)$
5	4	adantr	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to P Fn (0 \dots M)$
6	3 5	syl6bi	$⊢ M \in ℕ \to (P \in RePart (M) \to P Fn (0 \dots M))$
7	1 2 6	sylc	$⊢ φ \to P Fn (0 \dots M)$
8	1 2	iccpartrn	$⊢ φ \to ran P \subseteq [P (0), P (M)]$
9		df-f	$⊢ P : (0 \dots M) ⟶ [P (0), P (M)] \leftrightarrow (P Fn (0 \dots M) \land ran P \subseteq [P (0), P (M)])$
10	7 8 9	sylanbrc	$⊢ φ \to P : (0 \dots M) ⟶ [P (0), P (M)]$