This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ W = N ClWWalksN G
erclwwlkn.r ⊢ ∼ ˙ = t u | t ∈ W ∧ u ∈ W ∧ ∃ n ∈ 0 … N t = u cyclShift n
Assertion qerclwwlknfi ⊢ Vtx ⁡ G ∈ Fin → W / ∼ ˙ ∈ Fin

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ W = N ClWWalksN G
2 erclwwlkn.r ⊢ ∼ ˙ = t u | t ∈ W ∧ u ∈ W ∧ ∃ n ∈ 0 … N t = u cyclShift n
3 clwwlknfi ⊢ Vtx ⁡ G ∈ Fin → N ClWWalksN G ∈ Fin
4 1 3 eqeltrid ⊢ Vtx ⁡ G ∈ Fin → W ∈ Fin
5 pwfi ⊢ W ∈ Fin ↔ 𝒫 W ∈ Fin
6 4 5 sylib ⊢ Vtx ⁡ G ∈ Fin → 𝒫 W ∈ Fin
7 1 2 erclwwlkn ⊢ ∼ ˙ Er W
8 7 a1i ⊢ Vtx ⁡ G ∈ Fin → ∼ ˙ Er W
9 8 qsss ⊢ Vtx ⁡ G ∈ Fin → W / ∼ ˙ ⊆ 𝒫 W
10 6 9 ssfid ⊢ Vtx ⁡ G ∈ Fin → W / ∼ ˙ ∈ Fin