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 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡𝑊𝑢𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion eclclwwlkn1 ( 𝐵𝑋 → ( 𝐵 ∈ ( 𝑊 / ) ↔ ∃ 𝑥𝑊 𝐵 = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡𝑊𝑢𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 elqsecl ( 𝐵𝑋 → ( 𝐵 ∈ ( 𝑊 / ) ↔ ∃ 𝑥𝑊 𝐵 = { 𝑦𝑥 𝑦 } ) )
4 1 2 erclwwlknsym ( 𝑥 𝑦𝑦 𝑥 )
5 1 2 erclwwlknsym ( 𝑦 𝑥𝑥 𝑦 )
6 4 5 impbii ( 𝑥 𝑦𝑦 𝑥 )
7 6 a1i ( ( 𝐵𝑋𝑥𝑊 ) → ( 𝑥 𝑦𝑦 𝑥 ) )
8 7 abbidv ( ( 𝐵𝑋𝑥𝑊 ) → { 𝑦𝑥 𝑦 } = { 𝑦𝑦 𝑥 } )
9 1 2 erclwwlkneq ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 𝑥 ↔ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
10 9 el2v ( 𝑦 𝑥 ↔ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )
11 10 a1i ( ( 𝐵𝑋𝑥𝑊 ) → ( 𝑦 𝑥 ↔ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
12 11 abbidv ( ( 𝐵𝑋𝑥𝑊 ) → { 𝑦𝑦 𝑥 } = { 𝑦 ∣ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) } )
13 3anan12 ( ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑥𝑊 ∧ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
14 ibar ( 𝑥𝑊 → ( ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑥𝑊 ∧ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) ) )
15 14 bicomd ( 𝑥𝑊 → ( ( 𝑥𝑊 ∧ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) ↔ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
16 15 adantl ( ( 𝐵𝑋𝑥𝑊 ) → ( ( 𝑥𝑊 ∧ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) ↔ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
17 13 16 syl5bb ( ( 𝐵𝑋𝑥𝑊 ) → ( ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
18 17 abbidv ( ( 𝐵𝑋𝑥𝑊 ) → { 𝑦 ∣ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) } = { 𝑦 ∣ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) } )
19 df-rab { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∣ ( 𝑦𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) }
20 18 19 eqtr4di ( ( 𝐵𝑋𝑥𝑊 ) → { 𝑦 ∣ ( 𝑦𝑊𝑥𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) } = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
21 8 12 20 3eqtrd ( ( 𝐵𝑋𝑥𝑊 ) → { 𝑦𝑥 𝑦 } = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
22 21 eqeq2d ( ( 𝐵𝑋𝑥𝑊 ) → ( 𝐵 = { 𝑦𝑥 𝑦 } ↔ 𝐵 = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
23 22 rexbidva ( 𝐵𝑋 → ( ∃ 𝑥𝑊 𝐵 = { 𝑦𝑥 𝑦 } ↔ ∃ 𝑥𝑊 𝐵 = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
24 3 23 bitrd ( 𝐵𝑋 → ( 𝐵 ∈ ( 𝑊 / ) ↔ ∃ 𝑥𝑊 𝐵 = { 𝑦𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )