Step |
Hyp |
Ref |
Expression |
1 |
|
erclwwlkn.w |
⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 ) |
2 |
|
erclwwlkn.r |
⊢ ∼ = { 〈 𝑡 , 𝑢 〉 ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } |
3 |
|
clwwlknfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin ) |
4 |
1 3
|
eqeltrid |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → 𝑊 ∈ Fin ) |
5 |
|
pwfi |
⊢ ( 𝑊 ∈ Fin ↔ 𝒫 𝑊 ∈ Fin ) |
6 |
4 5
|
sylib |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → 𝒫 𝑊 ∈ Fin ) |
7 |
1 2
|
erclwwlkn |
⊢ ∼ Er 𝑊 |
8 |
7
|
a1i |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ∼ Er 𝑊 ) |
9 |
8
|
qsss |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑊 / ∼ ) ⊆ 𝒫 𝑊 ) |
10 |
6 9
|
ssfid |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑊 / ∼ ) ∈ Fin ) |