Metamath Proof Explorer


Theorem clwwlknwrd

Description: A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021)

Ref Expression
Hypothesis clwwlknwrd.v
|- V = ( Vtx ` G )
Assertion clwwlknwrd
|- ( W e. ( N ClWWalksN G ) -> W e. Word V )

Proof

Step Hyp Ref Expression
1 clwwlknwrd.v
 |-  V = ( Vtx ` G )
2 isclwwlkn
 |-  ( W e. ( N ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) )
3 1 clwwlkbp
 |-  ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )
4 3 simp2d
 |-  ( W e. ( ClWWalks ` G ) -> W e. Word V )
5 4 adantr
 |-  ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) -> W e. Word V )
6 2 5 sylbi
 |-  ( W e. ( N ClWWalksN G ) -> W e. Word V )