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