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

Metamath Proof Explorer

Theorem wlknwwlksnen

Description: In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Assertion wlknwwlksnen 
|- ( ( G e. USPGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } = { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N }
2 eqid 
 |-  ( N WWalksN G ) = ( N WWalksN G )
3 eqid 
 |-  ( w e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` w ) ) = ( w e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` w ) )
4 1 2 3 wlknwwlksnbij 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( w e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` w ) ) : { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> ( N WWalksN G ) )
5 fvex 
 |-  ( Walks ` G ) e. _V
6 5 rabex 
 |-  { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } e. _V
7 6 f1oen 
 |-  ( ( w e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` w ) ) : { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> ( N WWalksN G ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )
8 4 7 syl 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )