Metamath Proof Explorer

Theorem clwwlkn1loopb

Description: A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022)

Ref Expression
Assertion clwwlkn1loopb 
|- ( W e. ( 1 ClWWalksN G ) <-> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkn1 
 |-  ( W e. ( 1 ClWWalksN G ) <-> ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) )
2 wrdl1exs1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> E. v e. ( Vtx ` G ) W = <" v "> )
3 fveq1 
 |-  ( W = <" v "> -> ( W ` 0 ) = ( <" v "> ` 0 ) )
4 s1fv 
 |-  ( v e. ( Vtx ` G ) -> ( <" v "> ` 0 ) = v )
5 3 4 sylan9eq 
 |-  ( ( W = <" v "> /\ v e. ( Vtx ` G ) ) -> ( W ` 0 ) = v )
6 5 sneqd 
 |-  ( ( W = <" v "> /\ v e. ( Vtx ` G ) ) -> { ( W ` 0 ) } = { v } )
7 6 eleq1d 
 |-  ( ( W = <" v "> /\ v e. ( Vtx ` G ) ) -> ( { ( W ` 0 ) } e. ( Edg ` G ) <-> { v } e. ( Edg ` G ) ) )
8 7 biimpd 
 |-  ( ( W = <" v "> /\ v e. ( Vtx ` G ) ) -> ( { ( W ` 0 ) } e. ( Edg ` G ) -> { v } e. ( Edg ` G ) ) )
9 8 ex 
 |-  ( W = <" v "> -> ( v e. ( Vtx ` G ) -> ( { ( W ` 0 ) } e. ( Edg ` G ) -> { v } e. ( Edg ` G ) ) ) )
10 9 com13 
 |-  ( { ( W ` 0 ) } e. ( Edg ` G ) -> ( v e. ( Vtx ` G ) -> ( W = <" v "> -> { v } e. ( Edg ` G ) ) ) )
11 10 imp 
 |-  ( ( { ( W ` 0 ) } e. ( Edg ` G ) /\ v e. ( Vtx ` G ) ) -> ( W = <" v "> -> { v } e. ( Edg ` G ) ) )
12 11 ancld 
 |-  ( ( { ( W ` 0 ) } e. ( Edg ` G ) /\ v e. ( Vtx ` G ) ) -> ( W = <" v "> -> ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) )
13 12 reximdva 
 |-  ( { ( W ` 0 ) } e. ( Edg ` G ) -> ( E. v e. ( Vtx ` G ) W = <" v "> -> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) )
14 2 13 syl5com 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> ( { ( W ` 0 ) } e. ( Edg ` G ) -> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) )
15 14 expcom 
 |-  ( ( # ` W ) = 1 -> ( W e. Word ( Vtx ` G ) -> ( { ( W ` 0 ) } e. ( Edg ` G ) -> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) ) )
16 15 3imp 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) -> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) )
17 s1len 
 |-  ( # ` <" v "> ) = 1
18 17 a1i 
 |-  ( ( v e. ( Vtx ` G ) /\ { v } e. ( Edg ` G ) ) -> ( # ` <" v "> ) = 1 )
19 s1cl 
 |-  ( v e. ( Vtx ` G ) -> <" v "> e. Word ( Vtx ` G ) )
20 19 adantr 
 |-  ( ( v e. ( Vtx ` G ) /\ { v } e. ( Edg ` G ) ) -> <" v "> e. Word ( Vtx ` G ) )
21 4 eqcomd 
 |-  ( v e. ( Vtx ` G ) -> v = ( <" v "> ` 0 ) )
22 21 sneqd 
 |-  ( v e. ( Vtx ` G ) -> { v } = { ( <" v "> ` 0 ) } )
23 22 eleq1d 
 |-  ( v e. ( Vtx ` G ) -> ( { v } e. ( Edg ` G ) <-> { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) )
24 23 biimpd 
 |-  ( v e. ( Vtx ` G ) -> ( { v } e. ( Edg ` G ) -> { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) )
25 24 imp 
 |-  ( ( v e. ( Vtx ` G ) /\ { v } e. ( Edg ` G ) ) -> { ( <" v "> ` 0 ) } e. ( Edg ` G ) )
26 18 20 25 3jca 
 |-  ( ( v e. ( Vtx ` G ) /\ { v } e. ( Edg ` G ) ) -> ( ( # ` <" v "> ) = 1 /\ <" v "> e. Word ( Vtx ` G ) /\ { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) )
27 26 adantrl 
 |-  ( ( v e. ( Vtx ` G ) /\ ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) -> ( ( # ` <" v "> ) = 1 /\ <" v "> e. Word ( Vtx ` G ) /\ { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) )
28 fveqeq2 
 |-  ( W = <" v "> -> ( ( # ` W ) = 1 <-> ( # ` <" v "> ) = 1 ) )
29 eleq1 
 |-  ( W = <" v "> -> ( W e. Word ( Vtx ` G ) <-> <" v "> e. Word ( Vtx ` G ) ) )
30 3 sneqd 
 |-  ( W = <" v "> -> { ( W ` 0 ) } = { ( <" v "> ` 0 ) } )
31 30 eleq1d 
 |-  ( W = <" v "> -> ( { ( W ` 0 ) } e. ( Edg ` G ) <-> { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) )
32 28 29 31 3anbi123d 
 |-  ( W = <" v "> -> ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( ( # ` <" v "> ) = 1 /\ <" v "> e. Word ( Vtx ` G ) /\ { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) ) )
33 32 ad2antrl 
 |-  ( ( v e. ( Vtx ` G ) /\ ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) -> ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( ( # ` <" v "> ) = 1 /\ <" v "> e. Word ( Vtx ` G ) /\ { ( <" v "> ` 0 ) } e. ( Edg ` G ) ) ) )
34 27 33 mpbird 
 |-  ( ( v e. ( Vtx ` G ) /\ ( W = <" v "> /\ { v } e. ( Edg ` G ) ) ) -> ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) )
35 34 rexlimiva 
 |-  ( E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) -> ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) )
36 16 35 impbii 
 |-  ( ( ( # ` W ) = 1 /\ W e. Word ( Vtx ` G ) /\ { ( W ` 0 ) } e. ( Edg ` G ) ) <-> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) )
37 1 36 bitri 
 |-  ( W e. ( 1 ClWWalksN G ) <-> E. v e. ( Vtx ` G ) ( W = <" v "> /\ { v } e. ( Edg ` G ) ) )