Metamath Proof Explorer

Theorem wlknwwlksneqs

Description: The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 15-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		wlknwwlksnen	\|- ( ( G e. USPGraph /\ N e. NN0 ) -> { p e. ( Walks ` G ) \| ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )
2		hasheni	\|- ( { p e. ( Walks ` G ) \| ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) -> ( # ` { p e. ( Walks ` G ) \| ( # ` ( 1st ` p ) ) = N } ) = ( # ` ( N WWalksN G ) ) )
3	1 2	syl	\|- ( ( G e. USPGraph /\ N e. NN0 ) -> ( # ` { p e. ( Walks ` G ) \| ( # ` ( 1st ` p ) ) = N } ) = ( # ` ( N WWalksN G ) ) )

Step

Hyp

Ref

Expression

wlknwwlksnen

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

hasheni

 |-  ( { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) -> ( # ` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) = ( # ` ( N WWalksN G ) ) )

1 2

syl

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