This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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