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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion	qerclwwlknfi	|- ( ( Vtx ` G ) e. Fin -> ( W /. .~ ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	|- W = ( N ClWWalksN G )
2		erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3		clwwlknfi	|- ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin )
4	1 3	eqeltrid	|- ( ( Vtx ` G ) e. Fin -> W e. Fin )
5		pwfi	|- ( W e. Fin <-> ~P W e. Fin )
6	4 5	sylib	|- ( ( Vtx ` G ) e. Fin -> ~P W e. Fin )
7	1 2	erclwwlkn	|- .~ Er W
8	7	a1i	|- ( ( Vtx ` G ) e. Fin -> .~ Er W )
9	8	qsss	|- ( ( Vtx ` G ) e. Fin -> ( W /. .~ ) C_ ~P W )
10	6 9	ssfid	|- ( ( Vtx ` G ) e. Fin -> ( W /. .~ ) e. Fin )