Metamath Proof Explorer

Theorem iccpartiun

Description: A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m 
|- ( ph -> M e. NN )
iccpartiun.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartiun 
|- ( ph -> ( ( P ` 0 ) [,) ( P ` M ) ) = U_ 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 iccelpart 
 |-  ( M e. NN -> A. p e. ( RePart ` M ) ( x e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
4 fveq1 
 |-  ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
5 fveq1 
 |-  ( p = P -> ( p ` M ) = ( P ` M ) )
6 4 5 oveq12d 
 |-  ( p = P -> ( ( p ` 0 ) [,) ( p ` M ) ) = ( ( P ` 0 ) [,) ( P ` M ) ) )
7 6 eleq2d 
 |-  ( p = P -> ( x e. ( ( p ` 0 ) [,) ( p ` M ) ) <-> x e. ( ( P ` 0 ) [,) ( P ` M ) ) ) )
8 fveq1 
 |-  ( p = P -> ( p ` i ) = ( P ` i ) )
9 fveq1 
 |-  ( p = P -> ( p ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
10 8 9 oveq12d 
 |-  ( p = P -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
11 10 eleq2d 
 |-  ( p = P -> ( x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
12 11 rexbidv 
 |-  ( p = P -> ( E. i e. ( 0 ..^ M ) x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
13 7 12 imbi12d 
 |-  ( p = P -> ( ( x e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) ) )
14 13 rspcva 
 |-  ( ( P e. ( RePart ` M ) /\ A. p e. ( RePart ` M ) ( x e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
15 14 expcom 
 |-  ( A. p e. ( RePart ` M ) ( x e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( P e. ( RePart ` M ) -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) ) )
16 1 3 15 3syl 
 |-  ( ph -> ( P e. ( RePart ` M ) -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) ) )
17 2 16 mpd 
 |-  ( ph -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) -> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
18 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
19 0elfz 
 |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )
20 1 18 19 3syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
21 1 2 20 iccpartxr 
 |-  ( ph -> ( P ` 0 ) e. RR* )
22 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
23 22 biimpi 
 |-  ( M e. NN0 -> M e. ( 0 ... M ) )
24 1 18 23 3syl 
 |-  ( ph -> M e. ( 0 ... M ) )
25 1 2 24 iccpartxr 
 |-  ( ph -> ( P ` M ) e. RR* )
26 21 25 jca 
 |-  ( ph -> ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) )
27 26 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( P ` 0 ) e. RR* /\ ( P ` M ) e. RR* ) )
28 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
29 1 2 iccpartgel 
 |-  ( ph -> A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) )
30 fveq2 
 |-  ( j = i -> ( P ` j ) = ( P ` i ) )
31 30 breq2d 
 |-  ( j = i -> ( ( P ` 0 ) <_ ( P ` j ) <-> ( P ` 0 ) <_ ( P ` i ) ) )
32 31 rspcva 
 |-  ( ( i e. ( 0 ... M ) /\ A. j e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` j ) ) -> ( P ` 0 ) <_ ( P ` i ) )
33 28 29 32 syl2anr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` 0 ) <_ ( P ` i ) )
34 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
35 1 2 iccpartleu 
 |-  ( ph -> A. k e. ( 0 ... M ) ( P ` k ) <_ ( P ` M ) )
36 fveq2 
 |-  ( k = ( i + 1 ) -> ( P ` k ) = ( P ` ( i + 1 ) ) )
37 36 breq1d 
 |-  ( k = ( i + 1 ) -> ( ( P ` k ) <_ ( P ` M ) <-> ( P ` ( i + 1 ) ) <_ ( P ` M ) ) )
38 37 rspcva 
 |-  ( ( ( i + 1 ) e. ( 0 ... M ) /\ A. k e. ( 0 ... M ) ( P ` k ) <_ ( P ` M ) ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) )
39 34 35 38 syl2anr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` ( i + 1 ) ) <_ ( P ` M ) )
40 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 ) ) )
41 27 33 39 40 syl12anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) C_ ( ( P ` 0 ) [,) ( P ` M ) ) )
42 41 sseld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> x e. ( ( P ` 0 ) [,) ( P ` M ) ) ) )
43 42 rexlimdva 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) -> x e. ( ( P ` 0 ) [,) ( P ` M ) ) ) )
44 17 43 impbid 
 |-  ( ph -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) <-> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
45 eliun 
 |-  ( x e. U_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> E. i e. ( 0 ..^ M ) x e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
46 44 45 bitr4di 
 |-  ( ph -> ( x e. ( ( P ` 0 ) [,) ( P ` M ) ) <-> x e. U_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
47 46 eqrdv 
 |-  ( ph -> ( ( P ` 0 ) [,) ( P ` M ) ) = U_ i e. ( 0 ..^ M ) ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )