Theorem clwwlknonfin

Description: In a finite graph G , the set of closed walks on vertex X of length N is also finite. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

	Ref	Expression
Hypothesis	clwwlknonfin.v	|- V = ( Vtx ` G )
Assertion	clwwlknonfin	|- ( V e. Fin -> ( X ( ClWWalksNOn ` G ) N ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		clwwlknonfin.v	|- V = ( Vtx ` G )
2		clwwlknon	|- ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }
3	1	eleq1i	|- ( V e. Fin <-> ( Vtx ` G ) e. Fin )
4		clwwlknfi	|- ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin )
5	3 4	sylbi	|- ( V e. Fin -> ( N ClWWalksN G ) e. Fin )
6		rabfi	|- ( ( N ClWWalksN G ) e. Fin -> { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } e. Fin )
7	5 6	syl	|- ( V e. Fin -> { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } e. Fin )
8	2 7	eqeltrid	|- ( V e. Fin -> ( X ( ClWWalksNOn ` G ) N ) e. Fin )