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 biimtrdi 
 |-  ( ( # ` 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 ) ) )