| Step |
Hyp |
Ref |
Expression |
| 1 |
|
wlkp1.v |
|- V = ( Vtx ` G ) |
| 2 |
|
wlkp1.i |
|- I = ( iEdg ` G ) |
| 3 |
|
wlkp1.f |
|- ( ph -> Fun I ) |
| 4 |
|
wlkp1.a |
|- ( ph -> I e. Fin ) |
| 5 |
|
wlkp1.b |
|- ( ph -> B e. W ) |
| 6 |
|
wlkp1.c |
|- ( ph -> C e. V ) |
| 7 |
|
wlkp1.d |
|- ( ph -> -. B e. dom I ) |
| 8 |
|
wlkp1.w |
|- ( ph -> F ( Walks ` G ) P ) |
| 9 |
|
wlkp1.n |
|- N = ( # ` F ) |
| 10 |
|
wlkcl |
|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 ) |
| 11 |
1
|
wlkp |
|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V ) |
| 12 |
10 11
|
jca |
|- ( F ( Walks ` G ) P -> ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> V ) ) |
| 13 |
|
fzp1nel |
|- -. ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) ) |
| 14 |
13
|
a1i |
|- ( ( # ` F ) e. NN0 -> -. ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 15 |
9
|
oveq1i |
|- ( N + 1 ) = ( ( # ` F ) + 1 ) |
| 16 |
15
|
eleq1i |
|- ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 17 |
14 16
|
sylnibr |
|- ( ( # ` F ) e. NN0 -> -. ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 18 |
|
eleq2 |
|- ( dom P = ( 0 ... ( # ` F ) ) -> ( ( N + 1 ) e. dom P <-> ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) ) |
| 19 |
18
|
notbid |
|- ( dom P = ( 0 ... ( # ` F ) ) -> ( -. ( N + 1 ) e. dom P <-> -. ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) ) |
| 20 |
17 19
|
syl5ibrcom |
|- ( ( # ` F ) e. NN0 -> ( dom P = ( 0 ... ( # ` F ) ) -> -. ( N + 1 ) e. dom P ) ) |
| 21 |
|
fdm |
|- ( P : ( 0 ... ( # ` F ) ) --> V -> dom P = ( 0 ... ( # ` F ) ) ) |
| 22 |
20 21
|
impel |
|- ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> V ) -> -. ( N + 1 ) e. dom P ) |
| 23 |
8 12 22
|
3syl |
|- ( ph -> -. ( N + 1 ) e. dom P ) |