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 syl5ibr
 |-  ( 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 syl5ibr
 |-  ( ( 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 ) ) )