This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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