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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion eleclclwwlkn 
|- ( ( B e. ( W /. .~ ) /\ X e. B ) -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r 
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 1 2 eclclwwlkn1 
 |-  ( B e. ( W /. .~ ) -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
4 eqeq1 
 |-  ( y = Y -> ( y = ( x cyclShift n ) <-> Y = ( x cyclShift n ) ) )
5 4 rexbidv 
 |-  ( y = Y -> ( E. n e. ( 0 ... N ) y = ( x cyclShift n ) <-> E. n e. ( 0 ... N ) Y = ( x cyclShift n ) ) )
6 5 elrab 
 |-  ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 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 
 |-  ( E. n e. ( 0 ... N ) Y = ( x cyclShift n ) <-> E. k e. ( 0 ... N ) Y = ( x cyclShift k ) )
10 eqeq1 
 |-  ( y = X -> ( y = ( x cyclShift n ) <-> X = ( x cyclShift n ) ) )
11 10 rexbidv 
 |-  ( y = X -> ( E. n e. ( 0 ... N ) y = ( x cyclShift n ) <-> E. n e. ( 0 ... N ) X = ( x cyclShift n ) ) )
12 11 elrab 
 |-  ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( X e. W /\ E. n e. ( 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 
 |-  ( E. n e. ( 0 ... N ) X = ( x cyclShift n ) <-> E. m e. ( 0 ... N ) X = ( x cyclShift m ) )
16 1 eleclclwwlknlem2 
 |-  ( ( ( m e. ( 0 ... N ) /\ X = ( x cyclShift m ) ) /\ ( X e. W /\ x e. W ) ) -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
17 16 ex 
 |-  ( ( m e. ( 0 ... N ) /\ X = ( x cyclShift m ) ) -> ( ( X e. W /\ x e. W ) -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
18 17 rexlimiva 
 |-  ( E. m e. ( 0 ... N ) X = ( x cyclShift m ) -> ( ( X e. W /\ x e. W ) -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
19 15 18 sylbi 
 |-  ( E. n e. ( 0 ... N ) X = ( x cyclShift n ) -> ( ( X e. W /\ x e. W ) -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
20 19 expd 
 |-  ( E. n e. ( 0 ... N ) X = ( x cyclShift n ) -> ( X e. W -> ( x e. W -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) )
21 20 impcom 
 |-  ( ( X e. W /\ E. n e. ( 0 ... N ) X = ( x cyclShift n ) ) -> ( x e. W -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
22 12 21 sylbi 
 |-  ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( x e. W -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
23 22 com12 
 |-  ( x e. W -> ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
24 23 ad2antlr 
 |-  ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
25 24 imp 
 |-  ( ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) /\ X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( E. k e. ( 0 ... N ) Y = ( x cyclShift k ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
26 9 25 bitrid 
 |-  ( ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) /\ X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( E. n e. ( 0 ... N ) Y = ( x cyclShift n ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
27 26 anbi2d 
 |-  ( ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) /\ X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( x cyclShift n ) ) <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
28 6 27 bitrid 
 |-  ( ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) /\ X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
29 28 ex 
 |-  ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) )
30 eleq2 
 |-  ( B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( X e. B <-> X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
31 eleq2 
 |-  ( B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( Y e. B <-> Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
32 31 bibi1d 
 |-  ( B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) <-> ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) )
33 30 32 imbi12d 
 |-  ( B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) <-> ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) ) )
34 33 adantl 
 |-  ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) <-> ( X e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( Y e. { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) ) )
35 29 34 mpbird 
 |-  ( ( ( B e. ( W /. .~ ) /\ x e. W ) /\ B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) -> ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) )
36 35 rexlimdva2 
 |-  ( B e. ( W /. .~ ) -> ( E. x e. W B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) ) )
37 3 36 sylbid 
 |-  ( B e. ( W /. .~ ) -> ( B e. ( W /. .~ ) -> ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) ) )
38 37 pm2.43i 
 |-  ( B e. ( W /. .~ ) -> ( X e. B -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) ) )
39 38 imp 
 |-  ( ( B e. ( W /. .~ ) /\ X e. B ) -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )