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 )

Metamath Proof Explorer

Theorem qerclwwlknfi

Proof