Metamath Proof Explorer

Theorem clwwlknon2x

Description: The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Mar-2022)

Ref Expression
Hypotheses clwwlknon2.c 
|- C = ( ClWWalksNOn ` G )
clwwlknon2x.v 
|- V = ( Vtx ` G )
clwwlknon2x.e 
|- E = ( Edg ` G )
Assertion clwwlknon2x 
|- ( X C 2 ) = { w e. Word V | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }

Proof

Step Hyp Ref Expression
1 clwwlknon2.c 
 |-  C = ( ClWWalksNOn ` G )
2 clwwlknon2x.v 
 |-  V = ( Vtx ` G )
3 clwwlknon2x.e 
 |-  E = ( Edg ` G )
4 1 clwwlknon2 
 |-  ( X C 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }
5 clwwlkn2 
 |-  ( w e. ( 2 ClWWalksN G ) <-> ( ( # ` w ) = 2 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
6 5 anbi1i 
 |-  ( ( w e. ( 2 ClWWalksN G ) /\ ( w ` 0 ) = X ) <-> ( ( ( # ` w ) = 2 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) )
7 3anan12 
 |-  ( ( ( # ` w ) = 2 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) )
8 7 anbi1i 
 |-  ( ( ( ( # ` w ) = 2 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) <-> ( ( w e. Word ( Vtx ` G ) /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) /\ ( w ` 0 ) = X ) )
9 anass 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) /\ ( w ` 0 ) = X ) <-> ( w e. Word ( Vtx ` G ) /\ ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) )
10 2 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 df-3an 
 |-  ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) <-> ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E ) /\ ( w ` 0 ) = X ) )
14 3 eleq2i 
 |-  ( { ( w ` 0 ) , ( w ` 1 ) } e. E <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) )
15 14 anbi2i 
 |-  ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E ) <-> ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
16 15 anbi1i 
 |-  ( ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E ) /\ ( w ` 0 ) = X ) <-> ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) )
17 13 16 bitr2i 
 |-  ( ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) <-> ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) )
18 12 17 anbi12i 
 |-  ( ( w e. Word ( Vtx ` G ) /\ ( ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) ) )
19 9 18 bitri 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) ) /\ ( w ` 0 ) = X ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) ) )
20 8 19 bitri 
 |-  ( ( ( ( # ` w ) = 2 /\ w e. Word ( Vtx ` G ) /\ { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) /\ ( w ` 0 ) = X ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) ) )
21 6 20 bitri 
 |-  ( ( w e. ( 2 ClWWalksN G ) /\ ( w ` 0 ) = X ) <-> ( w e. Word V /\ ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) ) )
22 21 rabbia2 
 |-  { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X } = { w e. Word V | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }
23 4 22 eqtri 
 |-  ( X C 2 ) = { w e. Word V | ( ( # ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }