Metamath Proof Explorer

Theorem loopclwwlkn1b

Description: The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V . (Contributed by AV, 11-Feb-2022)

Ref Expression
Assertion loopclwwlkn1b 
|- ( V e. ( Vtx ` G ) -> ( { V } e. ( Edg ` G ) <-> <" V "> e. ( 1 ClWWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 clwwlkn1 
 |-  ( <" V "> e. ( 1 ClWWalksN G ) <-> ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) )
2 s1fv 
 |-  ( V e. ( Vtx ` G ) -> ( <" V "> ` 0 ) = V )
3 2 sneqd 
 |-  ( V e. ( Vtx ` G ) -> { ( <" V "> ` 0 ) } = { V } )
4 3 eleq1d 
 |-  ( V e. ( Vtx ` G ) -> ( { ( <" V "> ` 0 ) } e. ( Edg ` G ) <-> { V } e. ( Edg ` G ) ) )
5 4 biimpcd 
 |-  ( { ( <" V "> ` 0 ) } e. ( Edg ` G ) -> ( V e. ( Vtx ` G ) -> { V } e. ( Edg ` G ) ) )
6 5 3ad2ant3 
 |-  ( ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) -> ( V e. ( Vtx ` G ) -> { V } e. ( Edg ` G ) ) )
7 6 com12 
 |-  ( V e. ( Vtx ` G ) -> ( ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) -> { V } e. ( Edg ` G ) ) )
8 s1len 
 |-  ( # ` <" V "> ) = 1
9 8 a1i 
 |-  ( ( V e. ( Vtx ` G ) /\ { V } e. ( Edg ` G ) ) -> ( # ` <" V "> ) = 1 )
10 s1cl 
 |-  ( V e. ( Vtx ` G ) -> <" V "> e. Word ( Vtx ` G ) )
11 10 adantr 
 |-  ( ( V e. ( Vtx ` G ) /\ { V } e. ( Edg ` G ) ) -> <" V "> e. Word ( Vtx ` G ) )
12 2 eqcomd 
 |-  ( V e. ( Vtx ` G ) -> V = ( <" V "> ` 0 ) )
13 12 sneqd 
 |-  ( V e. ( Vtx ` G ) -> { V } = { ( <" V "> ` 0 ) } )
14 13 eleq1d 
 |-  ( V e. ( Vtx ` G ) -> ( { V } e. ( Edg ` G ) <-> { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) )
15 14 biimpa 
 |-  ( ( V e. ( Vtx ` G ) /\ { V } e. ( Edg ` G ) ) -> { ( <" V "> ` 0 ) } e. ( Edg ` G ) )
16 9 11 15 3jca 
 |-  ( ( V e. ( Vtx ` G ) /\ { V } e. ( Edg ` G ) ) -> ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) )
17 16 ex 
 |-  ( V e. ( Vtx ` G ) -> ( { V } e. ( Edg ` G ) -> ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) ) )
18 7 17 impbid 
 |-  ( V e. ( Vtx ` G ) -> ( ( ( # ` <" V "> ) = 1 /\ <" V "> e. Word ( Vtx ` G ) /\ { ( <" V "> ` 0 ) } e. ( Edg ` G ) ) <-> { V } e. ( Edg ` G ) ) )
19 1 18 bitr2id 
 |-  ( V e. ( Vtx ` G ) -> ( { V } e. ( Edg ` G ) <-> <" V "> e. ( 1 ClWWalksN G ) ) )