Step |
Hyp |
Ref |
Expression |
1 |
|
wlkcl |
|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 ) |
2 |
1
|
adantr |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> ( # ` F ) e. NN0 ) |
3 |
|
wlkiswwlks1 |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P -> P e. ( WWalks ` G ) ) ) |
4 |
3
|
com12 |
|- ( F ( Walks ` G ) P -> ( G e. UPGraph -> P e. ( WWalks ` G ) ) ) |
5 |
4
|
ad2antrl |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( G e. UPGraph -> P e. ( WWalks ` G ) ) ) |
6 |
5
|
imp |
|- ( ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) /\ G e. UPGraph ) -> P e. ( WWalks ` G ) ) |
7 |
|
wlklenvp1 |
|- ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
8 |
7
|
ad2antrl |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
9 |
|
oveq1 |
|- ( ( # ` F ) = N -> ( ( # ` F ) + 1 ) = ( N + 1 ) ) |
10 |
9
|
adantl |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> ( ( # ` F ) + 1 ) = ( N + 1 ) ) |
11 |
10
|
adantl |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( ( # ` F ) + 1 ) = ( N + 1 ) ) |
12 |
8 11
|
eqtrd |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( # ` P ) = ( N + 1 ) ) |
13 |
12
|
adantr |
|- ( ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) /\ G e. UPGraph ) -> ( # ` P ) = ( N + 1 ) ) |
14 |
|
eleq1 |
|- ( ( # ` F ) = N -> ( ( # ` F ) e. NN0 <-> N e. NN0 ) ) |
15 |
|
iswwlksn |
|- ( N e. NN0 -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) ) |
16 |
14 15
|
syl6bi |
|- ( ( # ` F ) = N -> ( ( # ` F ) e. NN0 -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) ) ) |
17 |
16
|
adantl |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> ( ( # ` F ) e. NN0 -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) ) ) |
18 |
17
|
impcom |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) ) |
19 |
18
|
adantr |
|- ( ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) /\ G e. UPGraph ) -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) ) |
20 |
6 13 19
|
mpbir2and |
|- ( ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) /\ G e. UPGraph ) -> P e. ( N WWalksN G ) ) |
21 |
20
|
ex |
|- ( ( ( # ` F ) e. NN0 /\ ( F ( Walks ` G ) P /\ ( # ` F ) = N ) ) -> ( G e. UPGraph -> P e. ( N WWalksN G ) ) ) |
22 |
2 21
|
mpancom |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> ( G e. UPGraph -> P e. ( N WWalksN G ) ) ) |
23 |
22
|
com12 |
|- ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> P e. ( N WWalksN G ) ) ) |