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 bitrid ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝑥 ∈ 𝑊 ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 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 𝑛 ) } ) )