Metamath Proof Explorer

Theorem clwwlknon1

Description: The set of closed walks on vertex X of length 1 in a graph G as words over the set of vertices. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

Ref Expression
Hypotheses clwwlknon1.v 
|- V = ( Vtx ` G )
clwwlknon1.c 
|- C = ( ClWWalksNOn ` G )
clwwlknon1.e 
|- E = ( Edg ` G )
Assertion clwwlknon1 
|- ( X e. V -> ( X C 1 ) = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )

Proof

Step Hyp Ref Expression
1 clwwlknon1.v 
 |-  V = ( Vtx ` G )
2 clwwlknon1.c 
 |-  C = ( ClWWalksNOn ` G )
3 clwwlknon1.e 
 |-  E = ( Edg ` G )
4 2 oveqi 
 |-  ( X C 1 ) = ( X ( ClWWalksNOn ` G ) 1 )
5 4 a1i 
 |-  ( X e. V -> ( X C 1 ) = ( X ( ClWWalksNOn ` G ) 1 ) )
6 clwwlknon 
 |-  ( X ( ClWWalksNOn ` G ) 1 ) = { w e. ( 1 ClWWalksN G ) | ( w ` 0 ) = X }
7 6 a1i 
 |-  ( X e. V -> ( X ( ClWWalksNOn ` G ) 1 ) = { w e. ( 1 ClWWalksN G ) | ( w ` 0 ) = X } )
8 clwwlkn1 
 |-  ( w e. ( 1 ClWWalksN G ) <-> ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) )
9 8 anbi1i 
 |-  ( ( w e. ( 1 ClWWalksN G ) /\ ( w ` 0 ) = X ) <-> ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) )
10 1 eqcomi 
 |-  ( Vtx ` G ) = V
11 10 wrdeqi 
 |-  Word ( Vtx ` G ) = Word V
12 11 eleq2i 
 |-  ( w e. Word ( Vtx ` G ) <-> w e. Word V )
13 12 biimpi 
 |-  ( w e. Word ( Vtx ` G ) -> w e. Word V )
14 13 3ad2ant2 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) -> w e. Word V )
15 14 ad2antrl 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> w e. Word V )
16 14 adantr 
 |-  ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) -> w e. Word V )
17 simpl1 
 |-  ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) -> ( # ` w ) = 1 )
18 simpr 
 |-  ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) -> ( w ` 0 ) = X )
19 16 17 18 3jca 
 |-  ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) -> ( w e. Word V /\ ( # ` w ) = 1 /\ ( w ` 0 ) = X ) )
20 19 adantl 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> ( w e. Word V /\ ( # ` w ) = 1 /\ ( w ` 0 ) = X ) )
21 wrdl1s1 
 |-  ( X e. V -> ( w = <" X "> <-> ( w e. Word V /\ ( # ` w ) = 1 /\ ( w ` 0 ) = X ) ) )
22 21 adantr 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> ( w = <" X "> <-> ( w e. Word V /\ ( # ` w ) = 1 /\ ( w ` 0 ) = X ) ) )
23 20 22 mpbird 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> w = <" X "> )
24 sneq 
 |-  ( ( w ` 0 ) = X -> { ( w ` 0 ) } = { X } )
25 3 eqcomi 
 |-  ( Edg ` G ) = E
26 25 a1i 
 |-  ( ( w ` 0 ) = X -> ( Edg ` G ) = E )
27 24 26 eleq12d 
 |-  ( ( w ` 0 ) = X -> ( { ( w ` 0 ) } e. ( Edg ` G ) <-> { X } e. E ) )
28 27 biimpd 
 |-  ( ( w ` 0 ) = X -> ( { ( w ` 0 ) } e. ( Edg ` G ) -> { X } e. E ) )
29 28 a1i 
 |-  ( X e. V -> ( ( w ` 0 ) = X -> ( { ( w ` 0 ) } e. ( Edg ` G ) -> { X } e. E ) ) )
30 29 com13 
 |-  ( { ( w ` 0 ) } e. ( Edg ` G ) -> ( ( w ` 0 ) = X -> ( X e. V -> { X } e. E ) ) )
31 30 3ad2ant3 
 |-  ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) -> ( ( w ` 0 ) = X -> ( X e. V -> { X } e. E ) ) )
32 31 imp 
 |-  ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) -> ( X e. V -> { X } e. E ) )
33 32 impcom 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> { X } e. E )
34 15 23 33 jca32 
 |-  ( ( X e. V /\ ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) -> ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) )
35 fveq2 
 |-  ( w = <" X "> -> ( # ` w ) = ( # ` <" X "> ) )
36 s1len 
 |-  ( # ` <" X "> ) = 1
37 35 36 eqtrdi 
 |-  ( w = <" X "> -> ( # ` w ) = 1 )
38 37 ad2antrl 
 |-  ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) -> ( # ` w ) = 1 )
39 38 adantl 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> ( # ` w ) = 1 )
40 1 wrdeqi 
 |-  Word V = Word ( Vtx ` G )
41 40 eleq2i 
 |-  ( w e. Word V <-> w e. Word ( Vtx ` G ) )
42 41 biimpi 
 |-  ( w e. Word V -> w e. Word ( Vtx ` G ) )
43 42 ad2antrl 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> w e. Word ( Vtx ` G ) )
44 fveq1 
 |-  ( w = <" X "> -> ( w ` 0 ) = ( <" X "> ` 0 ) )
45 s1fv 
 |-  ( X e. V -> ( <" X "> ` 0 ) = X )
46 44 45 sylan9eq 
 |-  ( ( w = <" X "> /\ X e. V ) -> ( w ` 0 ) = X )
47 46 eqcomd 
 |-  ( ( w = <" X "> /\ X e. V ) -> X = ( w ` 0 ) )
48 47 sneqd 
 |-  ( ( w = <" X "> /\ X e. V ) -> { X } = { ( w ` 0 ) } )
49 3 a1i 
 |-  ( ( w = <" X "> /\ X e. V ) -> E = ( Edg ` G ) )
50 48 49 eleq12d 
 |-  ( ( w = <" X "> /\ X e. V ) -> ( { X } e. E <-> { ( w ` 0 ) } e. ( Edg ` G ) ) )
51 50 biimpd 
 |-  ( ( w = <" X "> /\ X e. V ) -> ( { X } e. E -> { ( w ` 0 ) } e. ( Edg ` G ) ) )
52 51 impancom 
 |-  ( ( w = <" X "> /\ { X } e. E ) -> ( X e. V -> { ( w ` 0 ) } e. ( Edg ` G ) ) )
53 52 adantl 
 |-  ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) -> ( X e. V -> { ( w ` 0 ) } e. ( Edg ` G ) ) )
54 53 impcom 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> { ( w ` 0 ) } e. ( Edg ` G ) )
55 39 43 54 3jca 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) )
56 46 ex 
 |-  ( w = <" X "> -> ( X e. V -> ( w ` 0 ) = X ) )
57 56 ad2antrl 
 |-  ( ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) -> ( X e. V -> ( w ` 0 ) = X ) )
58 57 impcom 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> ( w ` 0 ) = X )
59 55 58 jca 
 |-  ( ( X e. V /\ ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) -> ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) )
60 34 59 impbida 
 |-  ( X e. V -> ( ( ( ( # ` w ) = 1 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) <-> ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) )
61 9 60 bitrid 
 |-  ( X e. V -> ( ( w e. ( 1 ClWWalksN G ) /\ ( w ` 0 ) = X ) <-> ( w e. Word V /\ ( w = <" X "> /\ { X } e. E ) ) ) )
62 61 rabbidva2 
 |-  ( X e. V -> { w e. ( 1 ClWWalksN G ) | ( w ` 0 ) = X } = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )
63 5 7 62 3eqtrd 
 |-  ( X e. V -> ( X C 1 ) = { w e. Word V | ( w = <" X "> /\ { X } e. E ) } )