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	|- ( ph -> M e. NN )
	iccpartgtprec.p	|- ( ph -> P e. ( RePart ` M ) )
Assertion	iccpartf	|- ( ph -> P : ( 0 ... M ) --> ( ( P ` 0 ) [,] ( P ` M ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	|- ( ph -> M e. NN )
2		iccpartgtprec.p	|- ( ph -> P e. ( RePart ` M ) )
3		iccpart	|- ( M e. NN -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
4		elmapfn	|- ( P e. ( RR* ^m ( 0 ... M ) ) -> P Fn ( 0 ... M ) )
5	4	adantr	|- ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> P Fn ( 0 ... M ) )
6	3 5	biimtrdi	|- ( M e. NN -> ( P e. ( RePart ` M ) -> P Fn ( 0 ... M ) ) )
7	1 2 6	sylc	|- ( ph -> P Fn ( 0 ... M ) )
8	1 2	iccpartrn	|- ( ph -> ran P C_ ( ( P ` 0 ) [,] ( P ` M ) ) )
9		df-f	|- ( P : ( 0 ... M ) --> ( ( P ` 0 ) [,] ( P ` M ) ) <-> ( P Fn ( 0 ... M ) /\ ran P C_ ( ( P ` 0 ) [,] ( P ` M ) ) ) )
10	7 8 9	sylanbrc	|- ( ph -> P : ( 0 ... M ) --> ( ( P ` 0 ) [,] ( P ` M ) ) )