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