Metamath Proof Explorer

Theorem clwwlk1loop

Description: A closed walk of length 1 is a loop. See also clwlkl1loop . (Contributed by AV, 24-Apr-2021)

Ref Expression
Assertion clwwlk1loop 
|- ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = 1 ) -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
4 lsw1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> ( lastS ` W ) = ( W ` 0 ) )
5 4 preq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` 0 ) , ( W ` 0 ) } )
6 5 eleq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
7 6 biimpd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
8 7 ex 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = 1 -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
9 8 com23 
 |-  ( W e. Word ( Vtx ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( # ` W ) = 1 -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
10 9 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( # ` W ) = 1 -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
11 10 imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( ( # ` W ) = 1 -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
12 11 3adant2 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( ( # ` W ) = 1 -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
13 3 12 sylbi 
 |-  ( W e. ( ClWWalks ` G ) -> ( ( # ` W ) = 1 -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
14 13 imp 
 |-  ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = 1 ) -> { ( W ` 0 ) , ( W ` 0 ) } e. ( Edg ` G ) )