Theorem clwwlken

Description: The set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length are equinumerous. (Contributed by AV, 5-Jun-2022) (Proof shortened by AV, 2-Nov-2022)

	Ref	Expression
Assertion	clwwlken	|- ( N e. NN -> { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } ~~ ( N ClWWalksN G ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	|- ( N WWalksN G ) e. _V
2	1	rabex	|- { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } e. _V
3		ovex	|- ( N ClWWalksN G ) e. _V
4		eqid	|- { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
5		eqid	|- ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) = ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) )
6	4 5	clwwlkf1o	|- ( N e. NN -> ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) : { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } -1-1-onto-> ( N ClWWalksN G ) )
7		f1oen2g	|- ( ( { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } e. _V /\ ( N ClWWalksN G ) e. _V /\ ( c e. { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } |-> ( c prefix N ) ) : { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } -1-1-onto-> ( N ClWWalksN G ) ) -> { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } ~~ ( N ClWWalksN G ) )
8	2 3 6 7	mp3an12i	|- ( N e. NN -> { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) } ~~ ( N ClWWalksN G ) )