Metamath Proof Explorer

Theorem iccpartrn

Description: If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartrn 
|- ( ph -> ran P C_ ( ( 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 1 3 syl 
 |-  ( ph -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
5 elmapfn 
 |-  ( P e. ( RR* ^m ( 0 ... M ) ) -> P Fn ( 0 ... M ) )
6 5 adantr 
 |-  ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> P Fn ( 0 ... M ) )
7 4 6 syl6bi 
 |-  ( ph -> ( P e. ( RePart ` M ) -> P Fn ( 0 ... M ) ) )
8 2 7 mpd 
 |-  ( ph -> P Fn ( 0 ... M ) )
9 fvelrnb 
 |-  ( P Fn ( 0 ... M ) -> ( p e. ran P <-> E. i e. ( 0 ... M ) ( P ` i ) = p ) )
10 8 9 syl 
 |-  ( ph -> ( p e. ran P <-> E. i e. ( 0 ... M ) ( P ` i ) = p ) )
11 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> M e. NN )
12 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> P e. ( RePart ` M ) )
13 simpr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( 0 ... M ) )
14 11 12 13 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( P ` i ) e. RR* )
15 1 2 iccpartgel 
 |-  ( ph -> A. k e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` k ) )
16 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
17 16 breq2d 
 |-  ( k = i -> ( ( P ` 0 ) <_ ( P ` k ) <-> ( P ` 0 ) <_ ( P ` i ) ) )
18 17 rspcva 
 |-  ( ( i e. ( 0 ... M ) /\ A. k e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` k ) ) -> ( P ` 0 ) <_ ( P ` i ) )
19 18 expcom 
 |-  ( A. k e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` k ) -> ( i e. ( 0 ... M ) -> ( P ` 0 ) <_ ( P ` i ) ) )
20 15 19 syl 
 |-  ( ph -> ( i e. ( 0 ... M ) -> ( P ` 0 ) <_ ( P ` i ) ) )
21 20 imp 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( P ` 0 ) <_ ( P ` i ) )
22 1 2 iccpartleu 
 |-  ( ph -> A. k e. ( 0 ... M ) ( P ` k ) <_ ( P ` M ) )
23 16 breq1d 
 |-  ( k = i -> ( ( P ` k ) <_ ( P ` M ) <-> ( P ` i ) <_ ( P ` M ) ) )
24 23 rspcva 
 |-  ( ( i e. ( 0 ... M ) /\ A. k e. ( 0 ... M ) ( P ` k ) <_ ( P ` M ) ) -> ( P ` i ) <_ ( P ` M ) )
25 24 expcom 
 |-  ( A. k e. ( 0 ... M ) ( P ` k ) <_ ( P ` M ) -> ( i e. ( 0 ... M ) -> ( P ` i ) <_ ( P ` M ) ) )
26 22 25 syl 
 |-  ( ph -> ( i e. ( 0 ... M ) -> ( P ` i ) <_ ( P ` M ) ) )
27 26 imp 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( P ` i ) <_ ( P ` M ) )
28 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
29 0elfz 
 |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )
30 1 28 29 3syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
31 1 2 30 iccpartxr 
 |-  ( ph -> ( P ` 0 ) e. RR* )
32 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
33 28 32 sylib 
 |-  ( M e. NN -> M e. ( 0 ... M ) )
34 1 33 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
35 1 2 34 iccpartxr 
 |-  ( ph -> ( P ` M ) e. RR* )
36 31 35 jca 
 |-  ( ph -> ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) )
37 36 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) )
38 elicc1 
 |-  ( ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) -> ( ( P ` i ) e. ( ( P ` 0 ) [,] ( P ` M ) ) <-> ( ( P ` i ) e. RR* /\ ( P ` 0 ) <_ ( P ` i ) /\ ( P ` i ) <_ ( P ` M ) ) ) )
39 37 38 syl 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( P ` i ) e. ( ( P ` 0 ) [,] ( P ` M ) ) <-> ( ( P ` i ) e. RR* /\ ( P ` 0 ) <_ ( P ` i ) /\ ( P ` i ) <_ ( P ` M ) ) ) )
40 14 21 27 39 mpbir3and 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( P ` i ) e. ( ( P ` 0 ) [,] ( P ` M ) ) )
41 eleq1 
 |-  ( ( P ` i ) = p -> ( ( P ` i ) e. ( ( P ` 0 ) [,] ( P ` M ) ) <-> p e. ( ( P ` 0 ) [,] ( P ` M ) ) ) )
42 40 41 syl5ibcom 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( P ` i ) = p -> p e. ( ( P ` 0 ) [,] ( P ` M ) ) ) )
43 42 rexlimdva 
 |-  ( ph -> ( E. i e. ( 0 ... M ) ( P ` i ) = p -> p e. ( ( P ` 0 ) [,] ( P ` M ) ) ) )
44 10 43 sylbid 
 |-  ( ph -> ( p e. ran P -> p e. ( ( P ` 0 ) [,] ( P ` M ) ) ) )
45 44 ssrdv 
 |-  ( ph -> ran P C_ ( ( P ` 0 ) [,] ( P ` M ) ) )