Metamath Proof Explorer

Theorem wlksnwwlknvbij

Description: There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Assertion wlksnwwlknvbij 
|- ( ( G e. USPGraph /\ N e. NN0 ) -> E. f f : { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Walks ` G ) e. _V
2 1 mptrabex 
 |-  ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) e. _V
3 2 resex 
 |-  ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) e. _V
4 eqid 
 |-  ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) = ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) )
5 eqid 
 |-  { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } = { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N }
6 eqid 
 |-  ( N WWalksN G ) = ( N WWalksN G )
7 5 6 4 wlknwwlksnbij 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) : { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } -1-1-onto-> ( N WWalksN G ) )
8 fveq1 
 |-  ( w = ( 2nd ` p ) -> ( w ` 0 ) = ( ( 2nd ` p ) ` 0 ) )
9 8 eqeq1d 
 |-  ( w = ( 2nd ` p ) -> ( ( w ` 0 ) = X <-> ( ( 2nd ` p ) ` 0 ) = X ) )
10 9 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } /\ w = ( 2nd ` p ) ) -> ( ( w ` 0 ) = X <-> ( ( 2nd ` p ) ` 0 ) = X ) )
11 4 7 10 f1oresrab 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
12 f1oeq1 
 |-  ( f = ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) -> ( f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } <-> ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) )
13 12 spcegv 
 |-  ( ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) e. _V -> ( ( ( p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } |-> ( 2nd ` p ) ) |` { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } ) : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } -> E. f f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) )
14 3 11 13 mpsyl 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> E. f f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )
15 2fveq3 
 |-  ( p = q -> ( # ` ( 1st ` p ) ) = ( # ` ( 1st ` q ) ) )
16 15 eqeq1d 
 |-  ( p = q -> ( ( # ` ( 1st ` p ) ) = N <-> ( # ` ( 1st ` q ) ) = N ) )
17 16 rabrabi 
 |-  { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } = { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) }
18 17 eqcomi 
 |-  { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } = { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X }
19 f1oeq2 
 |-  ( { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } = { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -> ( f : { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } <-> f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) )
20 18 19 mp1i 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( f : { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } <-> f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) )
21 20 exbidv 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( E. f f : { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } <-> E. f f : { p e. { q e. ( Walks ` G ) | ( # ` ( 1st ` q ) ) = N } | ( ( 2nd ` p ) ` 0 ) = X } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } ) )
22 14 21 mpbird 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> E. f f : { p e. ( Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = X } )