| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trlsegvdeg.v |
|- V = ( Vtx ` G ) |
| 2 |
|
trlsegvdeg.i |
|- I = ( iEdg ` G ) |
| 3 |
|
trlsegvdeg.f |
|- ( ph -> Fun I ) |
| 4 |
|
trlsegvdeg.n |
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
| 5 |
|
trlsegvdeg.u |
|- ( ph -> U e. V ) |
| 6 |
|
trlsegvdeg.w |
|- ( ph -> F ( Trails ` G ) P ) |
| 7 |
|
trliswlk |
|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P ) |
| 8 |
1
|
wlkpvtx |
|- ( F ( Walks ` G ) P -> ( N e. ( 0 ... ( # ` F ) ) -> ( P ` N ) e. V ) ) |
| 9 |
|
elfzofz |
|- ( N e. ( 0 ..^ ( # ` F ) ) -> N e. ( 0 ... ( # ` F ) ) ) |
| 10 |
8 9
|
impel |
|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` N ) e. V ) |
| 11 |
1
|
wlkpvtx |
|- ( F ( Walks ` G ) P -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) -> ( P ` ( N + 1 ) ) e. V ) ) |
| 12 |
|
fzofzp1 |
|- ( N e. ( 0 ..^ ( # ` F ) ) -> ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 13 |
11 12
|
impel |
|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` ( N + 1 ) ) e. V ) |
| 14 |
10 13
|
jca |
|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) |
| 15 |
14
|
ex |
|- ( F ( Walks ` G ) P -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) ) |
| 16 |
6 7 15
|
3syl |
|- ( ph -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) ) |
| 17 |
4 16
|
mpd |
|- ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) |