This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iccpartgt

Description: If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartgt 
|- ( ph -> A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( i < j -> ( P ` i ) < ( P ` j ) ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
4 elnn0uz 
 |-  ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )
5 3 4 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
6 fzpred 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( 0 ... M ) = ( { 0 } u. ( ( 0 + 1 ) ... M ) ) )
7 5 6 syl 
 |-  ( ph -> ( 0 ... M ) = ( { 0 } u. ( ( 0 + 1 ) ... M ) ) )
8 0p1e1 
 |-  ( 0 + 1 ) = 1
9 8 oveq1i 
 |-  ( ( 0 + 1 ) ... M ) = ( 1 ... M )
10 9 a1i 
 |-  ( ph -> ( ( 0 + 1 ) ... M ) = ( 1 ... M ) )
11 10 uneq2d 
 |-  ( ph -> ( { 0 } u. ( ( 0 + 1 ) ... M ) ) = ( { 0 } u. ( 1 ... M ) ) )
12 7 11 eqtrd 
 |-  ( ph -> ( 0 ... M ) = ( { 0 } u. ( 1 ... M ) ) )
13 12 eleq2d 
 |-  ( ph -> ( i e. ( 0 ... M ) <-> i e. ( { 0 } u. ( 1 ... M ) ) ) )
14 elun 
 |-  ( i e. ( { 0 } u. ( 1 ... M ) ) <-> ( i e. { 0 } \/ i e. ( 1 ... M ) ) )
15 velsn 
 |-  ( i e. { 0 } <-> i = 0 )
16 15 orbi1i 
 |-  ( ( i e. { 0 } \/ i e. ( 1 ... M ) ) <-> ( i = 0 \/ i e. ( 1 ... M ) ) )
17 14 16 bitri 
 |-  ( i e. ( { 0 } u. ( 1 ... M ) ) <-> ( i = 0 \/ i e. ( 1 ... M ) ) )
18 fzisfzounsn 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( 0 ... M ) = ( ( 0 ..^ M ) u. { M } ) )
19 5 18 syl 
 |-  ( ph -> ( 0 ... M ) = ( ( 0 ..^ M ) u. { M } ) )
20 19 eleq2d 
 |-  ( ph -> ( j e. ( 0 ... M ) <-> j e. ( ( 0 ..^ M ) u. { M } ) ) )
21 elun 
 |-  ( j e. ( ( 0 ..^ M ) u. { M } ) <-> ( j e. ( 0 ..^ M ) \/ j e. { M } ) )
22 velsn 
 |-  ( j e. { M } <-> j = M )
23 22 orbi2i 
 |-  ( ( j e. ( 0 ..^ M ) \/ j e. { M } ) <-> ( j e. ( 0 ..^ M ) \/ j = M ) )
24 21 23 bitri 
 |-  ( j e. ( ( 0 ..^ M ) u. { M } ) <-> ( j e. ( 0 ..^ M ) \/ j = M ) )
25 20 24 bitrdi 
 |-  ( ph -> ( j e. ( 0 ... M ) <-> ( j e. ( 0 ..^ M ) \/ j = M ) ) )
26 simpl 
 |-  ( ( j e. ( 0 ..^ M ) /\ 0 < j ) -> j e. ( 0 ..^ M ) )
27 simpr 
 |-  ( ( j e. ( 0 ..^ M ) /\ 0 < j ) -> 0 < j )
28 27 gt0ne0d 
 |-  ( ( j e. ( 0 ..^ M ) /\ 0 < j ) -> j =/= 0 )
29 fzo1fzo0n0 
 |-  ( j e. ( 1 ..^ M ) <-> ( j e. ( 0 ..^ M ) /\ j =/= 0 ) )
30 26 28 29 sylanbrc 
 |-  ( ( j e. ( 0 ..^ M ) /\ 0 < j ) -> j e. ( 1 ..^ M ) )
31 1 2 iccpartigtl 
 |-  ( ph -> A. k e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` k ) )
32 fveq2 
 |-  ( k = j -> ( P ` k ) = ( P ` j ) )
33 32 breq2d 
 |-  ( k = j -> ( ( P ` 0 ) < ( P ` k ) <-> ( P ` 0 ) < ( P ` j ) ) )
34 33 rspcv 
 |-  ( j e. ( 1 ..^ M ) -> ( A. k e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` k ) -> ( P ` 0 ) < ( P ` j ) ) )
35 30 31 34 syl2imc 
 |-  ( ph -> ( ( j e. ( 0 ..^ M ) /\ 0 < j ) -> ( P ` 0 ) < ( P ` j ) ) )
36 35 expd 
 |-  ( ph -> ( j e. ( 0 ..^ M ) -> ( 0 < j -> ( P ` 0 ) < ( P ` j ) ) ) )
37 36 impcom 
 |-  ( ( j e. ( 0 ..^ M ) /\ ph ) -> ( 0 < j -> ( P ` 0 ) < ( P ` j ) ) )
38 breq1 
 |-  ( i = 0 -> ( i < j <-> 0 < j ) )
39 fveq2 
 |-  ( i = 0 -> ( P ` i ) = ( P ` 0 ) )
40 39 breq1d 
 |-  ( i = 0 -> ( ( P ` i ) < ( P ` j ) <-> ( P ` 0 ) < ( P ` j ) ) )
41 38 40 imbi12d 
 |-  ( i = 0 -> ( ( i < j -> ( P ` i ) < ( P ` j ) ) <-> ( 0 < j -> ( P ` 0 ) < ( P ` j ) ) ) )
42 37 41 imbitrrid 
 |-  ( i = 0 -> ( ( j e. ( 0 ..^ M ) /\ ph ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) )
43 42 expd 
 |-  ( i = 0 -> ( j e. ( 0 ..^ M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
44 43 com12 
 |-  ( j e. ( 0 ..^ M ) -> ( i = 0 -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
45 1 2 iccpartlt 
 |-  ( ph -> ( P ` 0 ) < ( P ` M ) )
46 fveq2 
 |-  ( j = M -> ( P ` j ) = ( P ` M ) )
47 39 46 breqan12rd 
 |-  ( ( j = M /\ i = 0 ) -> ( ( P ` i ) < ( P ` j ) <-> ( P ` 0 ) < ( P ` M ) ) )
48 45 47 imbitrrid 
 |-  ( ( j = M /\ i = 0 ) -> ( ph -> ( P ` i ) < ( P ` j ) ) )
49 48 a1dd 
 |-  ( ( j = M /\ i = 0 ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) )
50 49 ex 
 |-  ( j = M -> ( i = 0 -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
51 44 50 jaoi 
 |-  ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( i = 0 -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
52 51 com12 
 |-  ( i = 0 -> ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
53 elfzelz 
 |-  ( i e. ( 1 ... M ) -> i e. ZZ )
54 53 ad3antlr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> i e. ZZ )
55 53 peano2zd 
 |-  ( i e. ( 1 ... M ) -> ( i + 1 ) e. ZZ )
56 55 ad2antlr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( i + 1 ) e. ZZ )
57 elfzoelz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ZZ )
58 57 ad2antrr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> j e. ZZ )
59 simpr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> i < j )
60 57 53 anim12ci 
 |-  ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) -> ( i e. ZZ /\ j e. ZZ ) )
61 60 adantr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( i e. ZZ /\ j e. ZZ ) )
62 zltp1le 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( i < j <-> ( i + 1 ) <_ j ) )
63 61 62 syl 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( i < j <-> ( i + 1 ) <_ j ) )
64 59 63 mpbid 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( i + 1 ) <_ j )
65 56 58 64 3jca 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( ( i + 1 ) e. ZZ /\ j e. ZZ /\ ( i + 1 ) <_ j ) )
66 65 adantr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( ( i + 1 ) e. ZZ /\ j e. ZZ /\ ( i + 1 ) <_ j ) )
67 eluz2 
 |-  ( j e. ( ZZ>= ` ( i + 1 ) ) <-> ( ( i + 1 ) e. ZZ /\ j e. ZZ /\ ( i + 1 ) <_ j ) )
68 66 67 sylibr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> j e. ( ZZ>= ` ( i + 1 ) ) )
69 1 ad2antlr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> M e. NN )
70 2 ad2antlr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> P e. ( RePart ` M ) )
71 1zzd 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> 1 e. ZZ )
72 elfzelz 
 |-  ( k e. ( i ... j ) -> k e. ZZ )
73 72 adantl 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k e. ZZ )
74 elfzle1 
 |-  ( i e. ( 1 ... M ) -> 1 <_ i )
75 elfzle1 
 |-  ( k e. ( i ... j ) -> i <_ k )
76 1red 
 |-  ( k e. ( i ... j ) -> 1 e. RR )
77 elfzel1 
 |-  ( k e. ( i ... j ) -> i e. ZZ )
78 77 zred 
 |-  ( k e. ( i ... j ) -> i e. RR )
79 72 zred 
 |-  ( k e. ( i ... j ) -> k e. RR )
80 letr 
 |-  ( ( 1 e. RR /\ i e. RR /\ k e. RR ) -> ( ( 1 <_ i /\ i <_ k ) -> 1 <_ k ) )
81 76 78 79 80 syl3anc 
 |-  ( k e. ( i ... j ) -> ( ( 1 <_ i /\ i <_ k ) -> 1 <_ k ) )
82 75 81 mpan2d 
 |-  ( k e. ( i ... j ) -> ( 1 <_ i -> 1 <_ k ) )
83 74 82 syl5com 
 |-  ( i e. ( 1 ... M ) -> ( k e. ( i ... j ) -> 1 <_ k ) )
84 83 ad3antlr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( k e. ( i ... j ) -> 1 <_ k ) )
85 84 imp 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> 1 <_ k )
86 eluz2 
 |-  ( k e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ k e. ZZ /\ 1 <_ k ) )
87 71 73 85 86 syl3anbrc 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k e. ( ZZ>= ` 1 ) )
88 elfzel2 
 |-  ( i e. ( 1 ... M ) -> M e. ZZ )
89 88 ad2antlr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> M e. ZZ )
90 89 ad2antrr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> M e. ZZ )
91 79 adantl 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k e. RR )
92 57 zred 
 |-  ( j e. ( 0 ..^ M ) -> j e. RR )
93 92 ad4antr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> j e. RR )
94 69 nnred 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> M e. RR )
95 elfzle2 
 |-  ( k e. ( i ... j ) -> k <_ j )
96 95 adantl 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k <_ j )
97 elfzolt2 
 |-  ( j e. ( 0 ..^ M ) -> j < M )
98 97 ad4antr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> j < M )
99 91 93 94 96 98 lelttrd 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k < M )
100 elfzo2 
 |-  ( k e. ( 1 ..^ M ) <-> ( k e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ k < M ) )
101 87 90 99 100 syl3anbrc 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> k e. ( 1 ..^ M ) )
102 69 70 101 iccpartipre 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... j ) ) -> ( P ` k ) e. RR )
103 1 ad2antlr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... ( j - 1 ) ) ) -> M e. NN )
104 2 ad2antlr 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... ( j - 1 ) ) ) -> P e. ( RePart ` M ) )
105 57 ad3antrrr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> j e. ZZ )
106 fzoval 
 |-  ( j e. ZZ -> ( i ..^ j ) = ( i ... ( j - 1 ) ) )
107 105 106 syl 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( i ..^ j ) = ( i ... ( j - 1 ) ) )
108 elfzo0le 
 |-  ( j e. ( 0 ..^ M ) -> j <_ M )
109 0le1 
 |-  0 <_ 1
110 0red 
 |-  ( i e. ( 1 ... M ) -> 0 e. RR )
111 1red 
 |-  ( i e. ( 1 ... M ) -> 1 e. RR )
112 53 zred 
 |-  ( i e. ( 1 ... M ) -> i e. RR )
113 letr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ i e. RR ) -> ( ( 0 <_ 1 /\ 1 <_ i ) -> 0 <_ i ) )
114 110 111 112 113 syl3anc 
 |-  ( i e. ( 1 ... M ) -> ( ( 0 <_ 1 /\ 1 <_ i ) -> 0 <_ i ) )
115 109 114 mpani 
 |-  ( i e. ( 1 ... M ) -> ( 1 <_ i -> 0 <_ i ) )
116 74 115 mpd 
 |-  ( i e. ( 1 ... M ) -> 0 <_ i )
117 108 116 anim12ci 
 |-  ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) -> ( 0 <_ i /\ j <_ M ) )
118 117 adantr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( 0 <_ i /\ j <_ M ) )
119 0zd 
 |-  ( j e. ( 0 ..^ M ) -> 0 e. ZZ )
120 elfzoel2 
 |-  ( j e. ( 0 ..^ M ) -> M e. ZZ )
121 119 120 jca 
 |-  ( j e. ( 0 ..^ M ) -> ( 0 e. ZZ /\ M e. ZZ ) )
122 121 ad2antrr 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( 0 e. ZZ /\ M e. ZZ ) )
123 ssfzo12bi 
 |-  ( ( ( i e. ZZ /\ j e. ZZ ) /\ ( 0 e. ZZ /\ M e. ZZ ) /\ i < j ) -> ( ( i ..^ j ) C_ ( 0 ..^ M ) <-> ( 0 <_ i /\ j <_ M ) ) )
124 61 122 59 123 syl3anc 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( ( i ..^ j ) C_ ( 0 ..^ M ) <-> ( 0 <_ i /\ j <_ M ) ) )
125 118 124 mpbird 
 |-  ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) -> ( i ..^ j ) C_ ( 0 ..^ M ) )
126 125 adantr 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( i ..^ j ) C_ ( 0 ..^ M ) )
127 107 126 eqsstrrd 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( i ... ( j - 1 ) ) C_ ( 0 ..^ M ) )
128 127 sselda 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... ( j - 1 ) ) ) -> k e. ( 0 ..^ M ) )
129 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ k e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
130 103 104 128 129 syl3anc 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... ( j - 1 ) ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
131 130 simprd 
 |-  ( ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) /\ k e. ( i ... ( j - 1 ) ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
132 54 68 102 131 smonoord 
 |-  ( ( ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) /\ i < j ) /\ ph ) -> ( P ` i ) < ( P ` j ) )
133 132 exp31 
 |-  ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) -> ( i < j -> ( ph -> ( P ` i ) < ( P ` j ) ) ) )
134 133 com23 
 |-  ( ( j e. ( 0 ..^ M ) /\ i e. ( 1 ... M ) ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) )
135 134 ex 
 |-  ( j e. ( 0 ..^ M ) -> ( i e. ( 1 ... M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
136 elfzuz 
 |-  ( i e. ( 1 ... M ) -> i e. ( ZZ>= ` 1 ) )
137 136 adantr 
 |-  ( ( i e. ( 1 ... M ) /\ i < M ) -> i e. ( ZZ>= ` 1 ) )
138 88 adantr 
 |-  ( ( i e. ( 1 ... M ) /\ i < M ) -> M e. ZZ )
139 simpr 
 |-  ( ( i e. ( 1 ... M ) /\ i < M ) -> i < M )
140 elfzo2 
 |-  ( i e. ( 1 ..^ M ) <-> ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) )
141 137 138 139 140 syl3anbrc 
 |-  ( ( i e. ( 1 ... M ) /\ i < M ) -> i e. ( 1 ..^ M ) )
142 1 2 iccpartiltu 
 |-  ( ph -> A. k e. ( 1 ..^ M ) ( P ` k ) < ( P ` M ) )
143 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
144 143 breq1d 
 |-  ( k = i -> ( ( P ` k ) < ( P ` M ) <-> ( P ` i ) < ( P ` M ) ) )
145 144 rspcv 
 |-  ( i e. ( 1 ..^ M ) -> ( A. k e. ( 1 ..^ M ) ( P ` k ) < ( P ` M ) -> ( P ` i ) < ( P ` M ) ) )
146 141 142 145 syl2imc 
 |-  ( ph -> ( ( i e. ( 1 ... M ) /\ i < M ) -> ( P ` i ) < ( P ` M ) ) )
147 146 expd 
 |-  ( ph -> ( i e. ( 1 ... M ) -> ( i < M -> ( P ` i ) < ( P ` M ) ) ) )
148 147 impcom 
 |-  ( ( i e. ( 1 ... M ) /\ ph ) -> ( i < M -> ( P ` i ) < ( P ` M ) ) )
149 148 imp 
 |-  ( ( ( i e. ( 1 ... M ) /\ ph ) /\ i < M ) -> ( P ` i ) < ( P ` M ) )
150 149 a1i 
 |-  ( j = M -> ( ( ( i e. ( 1 ... M ) /\ ph ) /\ i < M ) -> ( P ` i ) < ( P ` M ) ) )
151 breq2 
 |-  ( j = M -> ( i < j <-> i < M ) )
152 151 anbi2d 
 |-  ( j = M -> ( ( ( i e. ( 1 ... M ) /\ ph ) /\ i < j ) <-> ( ( i e. ( 1 ... M ) /\ ph ) /\ i < M ) ) )
153 46 breq2d 
 |-  ( j = M -> ( ( P ` i ) < ( P ` j ) <-> ( P ` i ) < ( P ` M ) ) )
154 150 152 153 3imtr4d 
 |-  ( j = M -> ( ( ( i e. ( 1 ... M ) /\ ph ) /\ i < j ) -> ( P ` i ) < ( P ` j ) ) )
155 154 exp4c 
 |-  ( j = M -> ( i e. ( 1 ... M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
156 135 155 jaoi 
 |-  ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( i e. ( 1 ... M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
157 156 com12 
 |-  ( i e. ( 1 ... M ) -> ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
158 52 157 jaoi 
 |-  ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( ph -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
159 158 com13 
 |-  ( ph -> ( ( j e. ( 0 ..^ M ) \/ j = M ) -> ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
160 25 159 sylbid 
 |-  ( ph -> ( j e. ( 0 ... M ) -> ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
161 160 com3r 
 |-  ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( ph -> ( j e. ( 0 ... M ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
162 17 161 sylbi 
 |-  ( i e. ( { 0 } u. ( 1 ... M ) ) -> ( ph -> ( j e. ( 0 ... M ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
163 162 com12 
 |-  ( ph -> ( i e. ( { 0 } u. ( 1 ... M ) ) -> ( j e. ( 0 ... M ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
164 13 163 sylbid 
 |-  ( ph -> ( i e. ( 0 ... M ) -> ( j e. ( 0 ... M ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) ) ) )
165 164 imp32 
 |-  ( ( ph /\ ( i e. ( 0 ... M ) /\ j e. ( 0 ... M ) ) ) -> ( i < j -> ( P ` i ) < ( P ` j ) ) )
166 165 ralrimivva 
 |-  ( ph -> A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( i < j -> ( P ` i ) < ( P ` j ) ) )