Metamath Proof Explorer


Theorem eleclclwwlkn

Description: A member of an equivalence class according to .~ . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 1-May-2021)

Ref Expression
Hypotheses erclwwlkn.w W = N ClWWalksN G
erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
Assertion eleclclwwlkn B W / ˙ X B Y B Y W n 0 N Y = X cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W = N ClWWalksN G
2 erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
3 1 2 eclclwwlkn1 B W / ˙ B W / ˙ x W B = y W | n 0 N y = x cyclShift n
4 eqeq1 y = Y y = x cyclShift n Y = x cyclShift n
5 4 rexbidv y = Y n 0 N y = x cyclShift n n 0 N Y = x cyclShift n
6 5 elrab Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = x cyclShift n
7 oveq2 n = k x cyclShift n = x cyclShift k
8 7 eqeq2d n = k Y = x cyclShift n Y = x cyclShift k
9 8 cbvrexvw n 0 N Y = x cyclShift n k 0 N Y = x cyclShift k
10 eqeq1 y = X y = x cyclShift n X = x cyclShift n
11 10 rexbidv y = X n 0 N y = x cyclShift n n 0 N X = x cyclShift n
12 11 elrab X y W | n 0 N y = x cyclShift n X W n 0 N X = x cyclShift n
13 oveq2 n = m x cyclShift n = x cyclShift m
14 13 eqeq2d n = m X = x cyclShift n X = x cyclShift m
15 14 cbvrexvw n 0 N X = x cyclShift n m 0 N X = x cyclShift m
16 1 eleclclwwlknlem2 m 0 N X = x cyclShift m X W x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
17 16 ex m 0 N X = x cyclShift m X W x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
18 17 rexlimiva m 0 N X = x cyclShift m X W x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
19 15 18 sylbi n 0 N X = x cyclShift n X W x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
20 19 expd n 0 N X = x cyclShift n X W x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
21 20 impcom X W n 0 N X = x cyclShift n x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
22 12 21 sylbi X y W | n 0 N y = x cyclShift n x W k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
23 22 com12 x W X y W | n 0 N y = x cyclShift n k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
24 23 ad2antlr B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
25 24 imp B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n k 0 N Y = x cyclShift k n 0 N Y = X cyclShift n
26 9 25 syl5bb B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n n 0 N Y = x cyclShift n n 0 N Y = X cyclShift n
27 26 anbi2d B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n Y W n 0 N Y = x cyclShift n Y W n 0 N Y = X cyclShift n
28 6 27 syl5bb B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = X cyclShift n
29 28 ex B W / ˙ x W B = y W | n 0 N y = x cyclShift n X y W | n 0 N y = x cyclShift n Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = X cyclShift n
30 eleq2 B = y W | n 0 N y = x cyclShift n X B X y W | n 0 N y = x cyclShift n
31 eleq2 B = y W | n 0 N y = x cyclShift n Y B Y y W | n 0 N y = x cyclShift n
32 31 bibi1d B = y W | n 0 N y = x cyclShift n Y B Y W n 0 N Y = X cyclShift n Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = X cyclShift n
33 30 32 imbi12d B = y W | n 0 N y = x cyclShift n X B Y B Y W n 0 N Y = X cyclShift n X y W | n 0 N y = x cyclShift n Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = X cyclShift n
34 33 adantl B W / ˙ x W B = y W | n 0 N y = x cyclShift n X B Y B Y W n 0 N Y = X cyclShift n X y W | n 0 N y = x cyclShift n Y y W | n 0 N y = x cyclShift n Y W n 0 N Y = X cyclShift n
35 29 34 mpbird B W / ˙ x W B = y W | n 0 N y = x cyclShift n X B Y B Y W n 0 N Y = X cyclShift n
36 35 rexlimdva2 B W / ˙ x W B = y W | n 0 N y = x cyclShift n X B Y B Y W n 0 N Y = X cyclShift n
37 3 36 sylbid B W / ˙ B W / ˙ X B Y B Y W n 0 N Y = X cyclShift n
38 37 pm2.43i B W / ˙ X B Y B Y W n 0 N Y = X cyclShift n
39 38 imp B W / ˙ X B Y B Y W n 0 N Y = X cyclShift n