Metamath Proof Explorer

Theorem erclwwlkrel

Description: .~ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Hypothesis erclwwlk.r 
|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion erclwwlkrel 
|- Rel .~

Proof

Step Hyp Ref Expression
1 erclwwlk.r 
 |-  .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
2 1 relopabi 
 |-  Rel .~