Metamath Proof Explorer


Theorem qerclwwlknfi

Description: The quotient set of the set of closed walks (defined as words) with a fixed length according to the equivalence relation .~ is finite. (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypotheses erclwwlkn.w 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡𝑊𝑢𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion qerclwwlknfi ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑊 / ) ∈ Fin )

Proof

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 )