Metamath Proof Explorer


Theorem iccpartres

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

Ref Expression
Assertion iccpartres
|- ( ( M e. NN /\ P e. ( RePart ` ( M + 1 ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RePart ` M ) )

Proof

Step Hyp Ref Expression
1 peano2nn
 |-  ( M e. NN -> ( M + 1 ) e. NN )
2 iccpart
 |-  ( ( M + 1 ) e. NN -> ( P e. ( RePart ` ( M + 1 ) ) <-> ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
3 1 2 syl
 |-  ( M e. NN -> ( P e. ( RePart ` ( M + 1 ) ) <-> ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
4 simpl
 |-  ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) )
5 nnz
 |-  ( M e. NN -> M e. ZZ )
6 uzid
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
7 5 6 syl
 |-  ( M e. NN -> M e. ( ZZ>= ` M ) )
8 peano2uz
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
9 7 8 syl
 |-  ( M e. NN -> ( M + 1 ) e. ( ZZ>= ` M ) )
10 fzss2
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( 0 ... M ) C_ ( 0 ... ( M + 1 ) ) )
11 9 10 syl
 |-  ( M e. NN -> ( 0 ... M ) C_ ( 0 ... ( M + 1 ) ) )
12 elmapssres
 |-  ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ ( 0 ... M ) C_ ( 0 ... ( M + 1 ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RR* ^m ( 0 ... M ) ) )
13 4 11 12 syl2anr
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RR* ^m ( 0 ... M ) ) )
14 fzoss2
 |-  ( ( M + 1 ) e. ( ZZ>= ` M ) -> ( 0 ..^ M ) C_ ( 0 ..^ ( M + 1 ) ) )
15 9 14 syl
 |-  ( M e. NN -> ( 0 ..^ M ) C_ ( 0 ..^ ( M + 1 ) ) )
16 ssralv
 |-  ( ( 0 ..^ M ) C_ ( 0 ..^ ( M + 1 ) ) -> ( A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
17 15 16 syl
 |-  ( M e. NN -> ( A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
18 17 adantld
 |-  ( M e. NN -> ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
19 18 imp
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) )
20 fzossfz
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
21 20 a1i
 |-  ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) -> ( 0 ..^ M ) C_ ( 0 ... M ) )
22 21 sselda
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
23 fvres
 |-  ( i e. ( 0 ... M ) -> ( ( P |` ( 0 ... M ) ) ` i ) = ( P ` i ) )
24 23 eqcomd
 |-  ( i e. ( 0 ... M ) -> ( P ` i ) = ( ( P |` ( 0 ... M ) ) ` i ) )
25 22 24 syl
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( P ` i ) = ( ( P |` ( 0 ... M ) ) ` i ) )
26 simpr
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
27 elfzouz
 |-  ( i e. ( 0 ..^ M ) -> i e. ( ZZ>= ` 0 ) )
28 27 adantl
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> i e. ( ZZ>= ` 0 ) )
29 fzofzp1b
 |-  ( i e. ( ZZ>= ` 0 ) -> ( i e. ( 0 ..^ M ) <-> ( i + 1 ) e. ( 0 ... M ) ) )
30 28 29 syl
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( i e. ( 0 ..^ M ) <-> ( i + 1 ) e. ( 0 ... M ) ) )
31 26 30 mpbid
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
32 fvres
 |-  ( ( i + 1 ) e. ( 0 ... M ) -> ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
33 31 32 syl
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
34 33 eqcomd
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( P ` ( i + 1 ) ) = ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) )
35 25 34 breq12d
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) )
36 35 biimpd
 |-  ( ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( P ` i ) < ( P ` ( i + 1 ) ) -> ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) )
37 36 ralimdva
 |-  ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ M e. NN ) -> ( A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) )
38 37 ex
 |-  ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) -> ( M e. NN -> ( A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) ) )
39 38 adantr
 |-  ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> ( M e. NN -> ( A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) ) )
40 39 impcom
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> ( A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) -> A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) )
41 19 40 mpd
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) )
42 iccpart
 |-  ( M e. NN -> ( ( P |` ( 0 ... M ) ) e. ( RePart ` M ) <-> ( ( P |` ( 0 ... M ) ) e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) ) )
43 42 adantr
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> ( ( P |` ( 0 ... M ) ) e. ( RePart ` M ) <-> ( ( P |` ( 0 ... M ) ) e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( ( P |` ( 0 ... M ) ) ` i ) < ( ( P |` ( 0 ... M ) ) ` ( i + 1 ) ) ) ) )
44 13 41 43 mpbir2and
 |-  ( ( M e. NN /\ ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RePart ` M ) )
45 44 ex
 |-  ( M e. NN -> ( ( P e. ( RR* ^m ( 0 ... ( M + 1 ) ) ) /\ A. i e. ( 0 ..^ ( M + 1 ) ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RePart ` M ) ) )
46 3 45 sylbid
 |-  ( M e. NN -> ( P e. ( RePart ` ( M + 1 ) ) -> ( P |` ( 0 ... M ) ) e. ( RePart ` M ) ) )
47 46 imp
 |-  ( ( M e. NN /\ P e. ( RePart ` ( M + 1 ) ) ) -> ( P |` ( 0 ... M ) ) e. ( RePart ` M ) )