Metamath Proof Explorer

Theorem icceuelpart

Description: An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m 
|- ( ph -> M e. NN )
iccpartiun.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion icceuelpart 
|- ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> E! i e. ( 0 ..^ M ) X e. ( ( 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 2 adantr 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> P e. ( RePart ` M ) )
4 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 ) ) ) ) )
5 1 4 syl 
 |-  ( ph -> A. p e. ( RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
6 5 adantr 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> A. p e. ( RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
7 fveq1 
 |-  ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
8 fveq1 
 |-  ( p = P -> ( p ` M ) = ( P ` M ) )
9 7 8 oveq12d 
 |-  ( p = P -> ( ( p ` 0 ) [,) ( p ` M ) ) = ( ( P ` 0 ) [,) ( P ` M ) ) )
10 9 eleq2d 
 |-  ( p = P -> ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) <-> X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) )
11 fveq1 
 |-  ( p = P -> ( p ` i ) = ( P ` i ) )
12 fveq1 
 |-  ( p = P -> ( p ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
13 11 12 oveq12d 
 |-  ( p = P -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
14 13 eleq2d 
 |-  ( p = P -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
15 14 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 ) ) ) ) )
16 10 15 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 ) ) ) ) ) )
17 16 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 ) ) ) ) )
18 17 adantld 
 |-  ( ( 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 ) ) ) ) ) -> ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
19 18 com12 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> ( ( 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 ) ) ) ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) ) )
20 3 6 19 mp2and 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> E. i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )
21 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> M e. NN )
22 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> P e. ( RePart ` M ) )
23 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
24 23 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
25 21 22 24 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` i ) e. RR* )
26 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
27 26 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
28 21 22 27 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` ( i + 1 ) ) e. RR* )
29 25 28 jca 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* ) )
30 29 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* ) )
31 elico1 
 |-  ( ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* ) -> ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) ) )
32 30 31 syl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) ) )
33 1 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> M e. NN )
34 2 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> P e. ( RePart ` M ) )
35 elfzofz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ( 0 ... M ) )
36 35 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
37 33 34 36 iccpartxr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( P ` j ) e. RR* )
38 fzofzp1 
 |-  ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
39 38 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
40 33 34 39 iccpartxr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( P ` ( j + 1 ) ) e. RR* )
41 37 40 jca 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( P ` j ) e. RR* /\ ( P ` ( j + 1 ) ) e. RR* ) )
42 41 adantrl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( P ` j ) e. RR* /\ ( P ` ( j + 1 ) ) e. RR* ) )
43 elico1 
 |-  ( ( ( P ` j ) e. RR* /\ ( P ` ( j + 1 ) ) e. RR* ) -> ( X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) <-> ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) )
44 42 43 syl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) <-> ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) )
45 32 44 anbi12d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) <-> ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) ) )
46 elfzoelz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ZZ )
47 46 zred 
 |-  ( i e. ( 0 ..^ M ) -> i e. RR )
48 elfzoelz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ZZ )
49 48 zred 
 |-  ( j e. ( 0 ..^ M ) -> j e. RR )
50 47 49 anim12i 
 |-  ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) -> ( i e. RR /\ j e. RR ) )
51 50 adantl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( i e. RR /\ j e. RR ) )
52 lttri4 
 |-  ( ( i e. RR /\ j e. RR ) -> ( i < j \/ i = j \/ j < i ) )
53 51 52 syl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( i < j \/ i = j \/ j < i ) )
54 1 2 icceuelpartlem 
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) -> ( i < j -> ( P ` ( i + 1 ) ) <_ ( P ` j ) ) ) )
55 54 imp31 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ i < j ) -> ( P ` ( i + 1 ) ) <_ ( P ` j ) )
56 simpl 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> X e. RR* )
57 28 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( P ` ( i + 1 ) ) e. RR* )
58 57 adantl 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( P ` ( i + 1 ) ) e. RR* )
59 37 adantrl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( P ` j ) e. RR* )
60 59 adantl 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( P ` j ) e. RR* )
61 nltle2tri 
 |-  ( ( X e. RR* /\ ( P ` ( i + 1 ) ) e. RR* /\ ( P ` j ) e. RR* ) -> -. ( X < ( P ` ( i + 1 ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) /\ ( P ` j ) <_ X ) )
62 56 58 60 61 syl3anc 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> -. ( X < ( P ` ( i + 1 ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) /\ ( P ` j ) <_ X ) )
63 62 pm2.21d 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( ( X < ( P ` ( i + 1 ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) /\ ( P ` j ) <_ X ) -> i = j ) )
64 63 3expd 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( X < ( P ` ( i + 1 ) ) -> ( ( P ` ( i + 1 ) ) <_ ( P ` j ) -> ( ( P ` j ) <_ X -> i = j ) ) ) )
65 64 ex 
 |-  ( X e. RR* -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( X < ( P ` ( i + 1 ) ) -> ( ( P ` ( i + 1 ) ) <_ ( P ` j ) -> ( ( P ` j ) <_ X -> i = j ) ) ) ) )
66 65 com23 
 |-  ( X e. RR* -> ( X < ( P ` ( i + 1 ) ) -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( P ` ( i + 1 ) ) <_ ( P ` j ) -> ( ( P ` j ) <_ X -> i = j ) ) ) ) )
67 66 com25 
 |-  ( X e. RR* -> ( ( P ` j ) <_ X -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( P ` ( i + 1 ) ) <_ ( P ` j ) -> ( X < ( P ` ( i + 1 ) ) -> i = j ) ) ) ) )
68 67 imp4b 
 |-  ( ( X e. RR* /\ ( P ` j ) <_ X ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> ( X < ( P ` ( i + 1 ) ) -> i = j ) ) )
69 68 com23 
 |-  ( ( X e. RR* /\ ( P ` j ) <_ X ) -> ( X < ( P ` ( i + 1 ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> i = j ) ) )
70 69 3adant3 
 |-  ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( X < ( P ` ( i + 1 ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> i = j ) ) )
71 70 com12 
 |-  ( X < ( P ` ( i + 1 ) ) -> ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> i = j ) ) )
72 71 3ad2ant3 
 |-  ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) -> ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> i = j ) ) )
73 72 imp 
 |-  ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> i = j ) )
74 73 com12 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( i + 1 ) ) <_ ( P ` j ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) )
75 55 74 syldan 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ i < j ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) )
76 75 expcom 
 |-  ( i < j -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) ) )
77 2a1 
 |-  ( i = j -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) ) )
78 1 2 icceuelpartlem 
 |-  ( ph -> ( ( j e. ( 0 ..^ M ) /\ i e. ( 0 ..^ M ) ) -> ( j < i -> ( P ` ( j + 1 ) ) <_ ( P ` i ) ) ) )
79 78 ancomsd 
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) -> ( j < i -> ( P ` ( j + 1 ) ) <_ ( P ` i ) ) ) )
80 79 imp31 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ j < i ) -> ( P ` ( j + 1 ) ) <_ ( P ` i ) )
81 40 adantrl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( P ` ( j + 1 ) ) e. RR* )
82 81 adantl 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( P ` ( j + 1 ) ) e. RR* )
83 25 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( P ` i ) e. RR* )
84 83 adantl 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( P ` i ) e. RR* )
85 nltle2tri 
 |-  ( ( X e. RR* /\ ( P ` ( j + 1 ) ) e. RR* /\ ( P ` i ) e. RR* ) -> -. ( X < ( P ` ( j + 1 ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) /\ ( P ` i ) <_ X ) )
86 56 82 84 85 syl3anc 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> -. ( X < ( P ` ( j + 1 ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) /\ ( P ` i ) <_ X ) )
87 86 pm2.21d 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( ( X < ( P ` ( j + 1 ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) /\ ( P ` i ) <_ X ) -> i = j ) )
88 87 3expd 
 |-  ( ( X e. RR* /\ ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) ) -> ( X < ( P ` ( j + 1 ) ) -> ( ( P ` ( j + 1 ) ) <_ ( P ` i ) -> ( ( P ` i ) <_ X -> i = j ) ) ) )
89 88 ex 
 |-  ( X e. RR* -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( X < ( P ` ( j + 1 ) ) -> ( ( P ` ( j + 1 ) ) <_ ( P ` i ) -> ( ( P ` i ) <_ X -> i = j ) ) ) ) )
90 89 com23 
 |-  ( X e. RR* -> ( X < ( P ` ( j + 1 ) ) -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( P ` ( j + 1 ) ) <_ ( P ` i ) -> ( ( P ` i ) <_ X -> i = j ) ) ) ) )
91 90 imp4b 
 |-  ( ( X e. RR* /\ X < ( P ` ( j + 1 ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> ( ( P ` i ) <_ X -> i = j ) ) )
92 91 com23 
 |-  ( ( X e. RR* /\ X < ( P ` ( j + 1 ) ) ) -> ( ( P ` i ) <_ X -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> i = j ) ) )
93 92 3adant2 
 |-  ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( ( P ` i ) <_ X -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> i = j ) ) )
94 93 com12 
 |-  ( ( P ` i ) <_ X -> ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> i = j ) ) )
95 94 3ad2ant2 
 |-  ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) -> ( ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> i = j ) ) )
96 95 imp 
 |-  ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> i = j ) )
97 96 com12 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ ( P ` ( j + 1 ) ) <_ ( P ` i ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) )
98 80 97 syldan 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) /\ j < i ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) )
99 98 expcom 
 |-  ( j < i -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) ) )
100 76 77 99 3jaoi 
 |-  ( ( i < j \/ i = j \/ j < i ) -> ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) ) )
101 53 100 mpcom 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( ( X e. RR* /\ ( P ` i ) <_ X /\ X < ( P ` ( i + 1 ) ) ) /\ ( X e. RR* /\ ( P ` j ) <_ X /\ X < ( P ` ( j + 1 ) ) ) ) -> i = j ) )
102 45 101 sylbid 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ j e. ( 0 ..^ M ) ) ) -> ( ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) -> i = j ) )
103 102 ralrimivva 
 |-  ( ph -> A. i e. ( 0 ..^ M ) A. j e. ( 0 ..^ M ) ( ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) -> i = j ) )
104 103 adantr 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> A. i e. ( 0 ..^ M ) A. j e. ( 0 ..^ M ) ( ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) -> i = j ) )
105 fveq2 
 |-  ( i = j -> ( P ` i ) = ( P ` j ) )
106 fvoveq1 
 |-  ( i = j -> ( P ` ( i + 1 ) ) = ( P ` ( j + 1 ) ) )
107 105 106 oveq12d 
 |-  ( i = j -> ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) = ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) )
108 107 eleq2d 
 |-  ( i = j -> ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) )
109 108 reu4 
 |-  ( E! i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) <-> ( E. i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ A. i e. ( 0 ..^ M ) A. j e. ( 0 ..^ M ) ( ( X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) /\ X e. ( ( P ` j ) [,) ( P ` ( j + 1 ) ) ) ) -> i = j ) ) )
110 20 104 109 sylanbrc 
 |-  ( ( ph /\ X e. ( ( P ` 0 ) [,) ( P ` M ) ) ) -> E! i e. ( 0 ..^ M ) X e. ( ( P ` i ) [,) ( P ` ( i + 1 ) ) ) )