Metamath Proof Explorer


Theorem wwlknbp

Description: Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018) (Revised by AV, 9-Apr-2021) (Proof shortened by AV, 20-May-2021)

Ref Expression
Hypothesis wwlkbp.v
|- V = ( Vtx ` G )
Assertion wwlknbp
|- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )

Proof

Step Hyp Ref Expression
1 wwlkbp.v
 |-  V = ( Vtx ` G )
2 df-wwlksn
 |-  WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
3 2 elmpocl
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ G e. _V ) )
4 simpl
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( N e. NN0 /\ G e. _V ) )
5 4 ancomd
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( G e. _V /\ N e. NN0 ) )
6 iswwlksn
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
7 6 adantr
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( W e. ( N WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
8 1 wwlkbp
 |-  ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word V ) )
9 8 simprd
 |-  ( W e. ( WWalks ` G ) -> W e. Word V )
10 9 adantr
 |-  ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word V )
11 7 10 syl6bi
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( W e. ( N WWalksN G ) -> W e. Word V ) )
12 11 imp
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> W e. Word V )
13 df-3an
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) <-> ( ( G e. _V /\ N e. NN0 ) /\ W e. Word V ) )
14 5 12 13 sylanbrc
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
15 3 14 mpancom
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )