Metamath Proof Explorer

Theorem iccpartdisj

Description: The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m 
|- ( ph -> M e. NN )
iccpartiun.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartdisj 
|- ( ph -> Disj_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpartiun.m 
 |-  ( ph -> M e. NN )
2 iccpartiun.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 nfv 
 |-  F/ i ph
4 nfreu1 
 |-  F/ i E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) )
5 simpl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ph )
6 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> M e. NN )
7 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> P e. ( RePart ` M ) )
8 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
9 0elfz 
 |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )
10 1 8 9 3syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
11 10 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> 0 e. ( 0 ... M ) )
12 6 7 11 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` 0 ) e. RR* )
13 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
14 13 biimpi 
 |-  ( M e. NN0 -> M e. ( 0 ... M ) )
15 1 8 14 3syl 
 |-  ( ph -> M e. ( 0 ... M ) )
16 15 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> M e. ( 0 ... M ) )
17 6 7 16 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` M ) e. RR* )
18 1 2 iccpartgel 
 |-  ( ph -> A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) )
19 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
20 19 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
21 fveq2 
 |-  ( j = i -> ( P ` j ) = ( P ` i ) )
22 21 breq2d 
 |-  ( j = i -> ( ( P ` 0 ) <_ ( P ` j ) <-> ( P ` 0 ) <_ ( P ` i ) ) )
23 22 rspcv 
 |-  ( i e. ( 0 ... M ) -> ( A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) -> ( P ` 0 ) <_ ( P ` i ) ) )
24 20 23 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) -> ( P ` 0 ) <_ ( P ` i ) ) )
25 24 ex 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) -> ( P ` 0 ) <_ ( P ` i ) ) ) )
26 18 25 mpid 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( P ` 0 ) <_ ( P ` i ) ) )
27 26 imp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` 0 ) <_ ( P ` i ) )
28 1 2 iccpartleu 
 |-  ( ph -> A. j e. ( 0 ... M ) ( P ` j ) <_ ( P ` M ) )
29 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
30 29 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
31 fveq2 
 |-  ( j = ( i + 1 ) -> ( P ` j ) = ( P ` ( i + 1 ) ) )
32 31 breq1d 
 |-  ( j = ( i + 1 ) -> ( ( P ` j ) <_ ( P ` M ) <-> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) )
33 32 rspcv 
 |-  ( ( i + 1 ) e. ( 0 ... M ) -> ( A. j e. ( 0 ... M ) ( P ` j ) <_ ( P ` M ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) )
34 30 33 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. j e. ( 0 ... M ) ( P ` j ) <_ ( P ` M ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) )
35 34 ex 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( A. j e. ( 0 ... M ) ( P ` j ) <_ ( P ` M ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) ) )
36 28 35 mpid 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) )
37 36 imp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) )
38 icossico 
 |-  ( ( ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) /\ ( ( P ` 0 ) <_ ( P ` i ) /\ ( P ` ( i + 1 ) ) <_ ( P ` M ) ) ) -> ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) C_ ( ( P ` 0 ) [,) ( P ` M ) ) )
39 12 17 27 37 38 syl22anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) C_ ( ( P ` 0 ) [,) ( P ` M ) ) )
40 39 sseld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> p e. ( ( P ` 0 ) [,) ( P ` M ) ) ) )
41 1 2 icceuelpart 
 |-  ( ( ph /\ p e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
42 5 40 41 syl6an 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
43 42 ex 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) ) )
44 3 4 43 rexlimd 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
45 rmo5 
 |-  ( E* i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> ( E. i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> E! i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
46 44 45 sylibr 
 |-  ( ph -> E* i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
47 46 alrimiv 
 |-  ( ph -> A. p E* i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
48 df-disj 
 |-  ( Disj_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> A. p E* i e. ( 0 ..^ M ) p e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
49 47 48 sylibr 
 |-  ( ph -> Disj_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )