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 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 )