Metamath Proof Explorer

Theorem eclclwwlkn1

Description: An equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-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 eclclwwlkn1 
|- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W 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 elqsecl 
 |-  ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y | x .~ y } ) )
4 1 2 erclwwlknsym 
 |-  ( x .~ y -> y .~ x )
5 1 2 erclwwlknsym 
 |-  ( y .~ x -> x .~ y )
6 4 5 impbii 
 |-  ( x .~ y <-> y .~ x )
7 6 a1i 
 |-  ( ( B e. X /\ x e. W ) -> ( x .~ y <-> y .~ x ) )
8 7 abbidv 
 |-  ( ( B e. X /\ x e. W ) -> { y | x .~ y } = { y | y .~ x } )
9 1 2 erclwwlkneq 
 |-  ( ( y e. _V /\ x e. _V ) -> ( y .~ x <-> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
10 9 el2v 
 |-  ( y .~ x <-> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) )
11 10 a1i 
 |-  ( ( B e. X /\ x e. W ) -> ( y .~ x <-> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
12 11 abbidv 
 |-  ( ( B e. X /\ x e. W ) -> { y | y .~ x } = { y | ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) } )
13 3anan12 
 |-  ( ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) <-> ( x e. W /\ ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
14 ibar 
 |-  ( x e. W -> ( ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) <-> ( x e. W /\ ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) ) )
15 14 bicomd 
 |-  ( x e. W -> ( ( x e. W /\ ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) <-> ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
16 15 adantl 
 |-  ( ( B e. X /\ x e. W ) -> ( ( x e. W /\ ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) <-> ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
17 13 16 bitrid 
 |-  ( ( B e. X /\ x e. W ) -> ( ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) <-> ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
18 17 abbidv 
 |-  ( ( B e. X /\ x e. W ) -> { y | ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) } = { y | ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) } )
19 df-rab 
 |-  { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y | ( y e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) }
20 18 19 eqtr4di 
 |-  ( ( B e. X /\ x e. W ) -> { y | ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) } = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
21 8 12 20 3eqtrd 
 |-  ( ( B e. X /\ x e. W ) -> { y | x .~ y } = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
22 21 eqeq2d 
 |-  ( ( B e. X /\ x e. W ) -> ( B = { y | x .~ y } <-> B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
23 22 rexbidva 
 |-  ( B e. X -> ( E. x e. W B = { y | x .~ y } <-> E. x e. W B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
24 3 23 bitrd 
 |-  ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )