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