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 𝑛 ) } ) ) |