Metamath Proof Explorer


Theorem wlklnwwlkln1

Description: The sequence of vertices in a walk of length N is a walk as word of length N in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wlklnwwlkln1
|- ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ ( # ` F ) = N ) -> P e. ( N WWalksN G ) ) )

Proof

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