| Step |
Hyp |
Ref |
Expression |
| 1 |
|
chnsubseq.1 |
|- ( ph -> W e. ( .< Chain A ) ) |
| 2 |
|
chnsubseq.2 |
|- ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) ) |
| 3 |
|
chnsubseq.3 |
|- ( ph -> .< Po A ) |
| 4 |
|
ltso |
|- < Or RR |
| 5 |
|
sopo |
|- ( < Or RR -> < Po RR ) |
| 6 |
4 5
|
mp1i |
|- ( ph -> < Po RR ) |
| 7 |
|
fzossz |
|- ( 0 ..^ ( # ` W ) ) C_ ZZ |
| 8 |
|
zssre |
|- ZZ C_ RR |
| 9 |
7 8
|
sstri |
|- ( 0 ..^ ( # ` W ) ) C_ RR |
| 10 |
9
|
a1i |
|- ( ph -> ( 0 ..^ ( # ` W ) ) C_ RR ) |
| 11 |
|
poss |
|- ( ( 0 ..^ ( # ` W ) ) C_ RR -> ( < Po RR -> < Po ( 0 ..^ ( # ` W ) ) ) ) |
| 12 |
10 11
|
syl |
|- ( ph -> ( < Po RR -> < Po ( 0 ..^ ( # ` W ) ) ) ) |
| 13 |
6 12
|
mpd |
|- ( ph -> < Po ( 0 ..^ ( # ` W ) ) ) |
| 14 |
|
ovexd |
|- ( ph -> ( 0 ..^ ( # ` W ) ) e. _V ) |
| 15 |
13 2 14
|
chnpolleha |
|- ( ph -> ( # ` I ) <_ ( # ` ( 0 ..^ ( # ` W ) ) ) ) |
| 16 |
1 2
|
chnsubseqwl |
|- ( ph -> ( # ` ( W o. I ) ) = ( # ` I ) ) |
| 17 |
1
|
chnwrd |
|- ( ph -> W e. Word A ) |
| 18 |
|
lencl |
|- ( W e. Word A -> ( # ` W ) e. NN0 ) |
| 19 |
17 18
|
syl |
|- ( ph -> ( # ` W ) e. NN0 ) |
| 20 |
|
hashfzo0 |
|- ( ( # ` W ) e. NN0 -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) ) |
| 21 |
19 20
|
syl |
|- ( ph -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) ) |
| 22 |
21
|
eqcomd |
|- ( ph -> ( # ` W ) = ( # ` ( 0 ..^ ( # ` W ) ) ) ) |
| 23 |
15 16 22
|
3brtr4d |
|- ( ph -> ( # ` ( W o. I ) ) <_ ( # ` W ) ) |