Metamath Proof Explorer


Theorem erclwwlknrel

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

Ref Expression
Hypotheses erclwwlkn.w W=NClWWalksNG
erclwwlkn.r ˙=tu|tWuWn0Nt=ucyclShiftn
Assertion erclwwlknrel Rel˙

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W=NClWWalksNG
2 erclwwlkn.r ˙=tu|tWuWn0Nt=ucyclShiftn
3 2 relopabi Rel˙