Metamath Proof Explorer

Theorem clwwlknlbonbgr1

Description: The last but one vertex in a closed walk is a neighbor of the first vertex of the closed walk. (Contributed by AV, 17-Feb-2022)

Ref Expression
Assertion clwwlknlbonbgr1 
|- ( ( G e. USGraph /\ W e. ( N ClWWalksN G ) ) -> ( W ` ( N - 1 ) ) e. ( G NeighbVtx ( W ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 clwwlknp 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
4 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
5 fvoveq1 
 |-  ( ( # ` W ) = N -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )
6 4 5 sylan9eq 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( lastS ` W ) = ( W ` ( N - 1 ) ) )
7 6 preq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
8 7 eleq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
9 8 biimpd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
10 9 a1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
11 10 3imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) )
12 3 11 syl 
 |-  ( W e. ( N ClWWalksN G ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) )
13 12 adantl 
 |-  ( ( G e. USGraph /\ W e. ( N ClWWalksN G ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) )
14 2 nbusgreledg 
 |-  ( G e. USGraph -> ( ( W ` ( N - 1 ) ) e. ( G NeighbVtx ( W ` 0 ) ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
15 14 adantr 
 |-  ( ( G e. USGraph /\ W e. ( N ClWWalksN G ) ) -> ( ( W ` ( N - 1 ) ) e. ( G NeighbVtx ( W ` 0 ) ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
16 13 15 mpbird 
 |-  ( ( G e. USGraph /\ W e. ( N ClWWalksN G ) ) -> ( W ` ( N - 1 ) ) e. ( G NeighbVtx ( W ` 0 ) ) )