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

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 1 2 eclclwwlkn1 ⊢ ( 𝐵 ∈ ( 𝑊 / ∼ ) → ( 𝐵 ∈ ( 𝑊 / ∼ ) ↔ ∃ 𝑥 ∈ 𝑊 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
4 eqeq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑌 = ( 𝑥 cyclShift 𝑛 ) ) )
5 4 rexbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑛 ) ) )
6 5 elrab ⊢ ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑛 ) ) )
7 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑘 ) )
8 7 eqeq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑌 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑌 = ( 𝑥 cyclShift 𝑘 ) ) )
9 8 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) )
10 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑋 = ( 𝑥 cyclShift 𝑛 ) ) )
11 10 rexbidv ⊢ ( 𝑦 = 𝑋 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) ) )
12 11 elrab ⊢ ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑋 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) ) )
13 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑚 ) )
14 13 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑋 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑋 = ( 𝑥 cyclShift 𝑚 ) ) )
15 14 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑚 ) )
16 1 eleclclwwlknlem2 ⊢ ( ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑚 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
17 16 ex ⊢ ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑚 ) ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
18 17 rexlimiva ⊢ ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑚 ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
19 15 18 sylbi ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
20 19 expd ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) → ( 𝑋 ∈ 𝑊 → ( 𝑥 ∈ 𝑊 → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
21 20 impcom ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑥 cyclShift 𝑛 ) ) → ( 𝑥 ∈ 𝑊 → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
22 12 21 sylbi ⊢ ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑥 ∈ 𝑊 → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
23 22 com12 ⊢ ( 𝑥 ∈ 𝑊 → ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
24 23 ad2antlr ⊢ ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
25 24 imp ⊢ ( ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) ∧ 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑘 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
26 9 25 syl5bb ⊢ ( ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) ∧ 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
27 26 anbi2d ⊢ ( ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) ∧ 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
28 6 27 syl5bb ⊢ ( ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) ∧ 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )
29 28 ex ⊢ ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
30 eleq2 ⊢ ( 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
31 eleq2 ⊢ ( 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
32 31 bibi1d ⊢ ( 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ↔ ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
33 30 32 imbi12d ⊢ ( 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ↔ ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
34 33 adantl ⊢ ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ↔ ( 𝑋 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑌 ∈ { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
35 29 34 mpbird ⊢ ( ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑥 ∈ 𝑊 ) ∧ 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
36 35 rexlimdva2 ⊢ ( 𝐵 ∈ ( 𝑊 / ∼ ) → ( ∃ 𝑥 ∈ 𝑊 𝐵 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
37 3 36 sylbid ⊢ ( 𝐵 ∈ ( 𝑊 / ∼ ) → ( 𝐵 ∈ ( 𝑊 / ∼ ) → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) ) )
38 37 pm2.43i ⊢ ( 𝐵 ∈ ( 𝑊 / ∼ ) → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) ) )
39 38 imp ⊢ ( ( 𝐵 ∈ ( 𝑊 / ∼ ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ↔ ( 𝑌 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) ) )