Metamath Proof Explorer

Theorem wlknwwlksnbij

Description: The mapping ( t e. T |-> ( 2ndt ) ) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Hypotheses wlknwwlksnbij.t 
|- T = { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N }
wlknwwlksnbij.w 
|- W = ( N WWalksN G )
wlknwwlksnbij.f 
|- F = ( t e. T |-> ( 2nd ` t ) )
Assertion wlknwwlksnbij 
|- ( ( G e. USPGraph /\ N e. NN0 ) -> F : T -1-1-onto-> W )

Proof

Step Hyp Ref Expression
1 wlknwwlksnbij.t 
 |-  T = { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N }
2 wlknwwlksnbij.w 
 |-  W = ( N WWalksN G )
3 wlknwwlksnbij.f 
 |-  F = ( t e. T |-> ( 2nd ` t ) )
4 eqid 
 |-  ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) = ( p e. ( Walks ` G ) |-> ( 2nd ` p ) )
5 4 wlkswwlksf1o 
 |-  ( G e. USPGraph -> ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) )
6 5 adantr 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) )
7 fveqeq2 
 |-  ( q = ( 2nd ` p ) -> ( ( # ` q ) = ( N + 1 ) <-> ( # ` ( 2nd ` p ) ) = ( N + 1 ) ) )
8 7 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ p e. ( Walks ` G ) /\ q = ( 2nd ` p ) ) -> ( ( # ` q ) = ( N + 1 ) <-> ( # ` ( 2nd ` p ) ) = ( N + 1 ) ) )
9 wlkcpr 
 |-  ( p e. ( Walks ` G ) <-> ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) )
10 wlklenvp1 
 |-  ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) -> ( # ` ( 2nd ` p ) ) = ( ( # ` ( 1st ` p ) ) + 1 ) )
11 eqeq1 
 |-  ( ( # ` ( 2nd ` p ) ) = ( ( # ` ( 1st ` p ) ) + 1 ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( ( # ` ( 1st ` p ) ) + 1 ) = ( N + 1 ) ) )
12 wlkcl 
 |-  ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) -> ( # ` ( 1st ` p ) ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) -> ( # ` ( 1st ` p ) ) e. CC )
14 13 adantr 
 |-  ( ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) /\ ( G e. USPGraph /\ N e. NN0 ) ) -> ( # ` ( 1st ` p ) ) e. CC )
15 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
16 15 adantl 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> N e. CC )
17 16 adantl 
 |-  ( ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) /\ ( G e. USPGraph /\ N e. NN0 ) ) -> N e. CC )
18 1cnd 
 |-  ( ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) /\ ( G e. USPGraph /\ N e. NN0 ) ) -> 1 e. CC )
19 14 17 18 addcan2d 
 |-  ( ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) /\ ( G e. USPGraph /\ N e. NN0 ) ) -> ( ( ( # ` ( 1st ` p ) ) + 1 ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) )
20 11 19 sylan9bbr 
 |-  ( ( ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) /\ ( G e. USPGraph /\ N e. NN0 ) ) /\ ( # ` ( 2nd ` p ) ) = ( ( # ` ( 1st ` p ) ) + 1 ) ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) )
21 20 exp31 
 |-  ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) -> ( ( G e. USPGraph /\ N e. NN0 ) -> ( ( # ` ( 2nd ` p ) ) = ( ( # ` ( 1st ` p ) ) + 1 ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) ) ) )
22 10 21 mpid 
 |-  ( ( 1st ` p ) ( Walks ` G ) ( 2nd ` p ) -> ( ( G e. USPGraph /\ N e. NN0 ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) ) )
23 9 22 sylbi 
 |-  ( p e. ( Walks ` G ) -> ( ( G e. USPGraph /\ N e. NN0 ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) ) )
24 23 impcom 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ p e. ( Walks ` G ) ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) )
25 24 3adant3 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ p e. ( Walks ` G ) /\ q = ( 2nd ` p ) ) -> ( ( # ` ( 2nd ` p ) ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) )
26 8 25 bitrd 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ p e. ( Walks ` G ) /\ q = ( 2nd ` p ) ) -> ( ( # ` q ) = ( N + 1 ) <-> ( # ` ( 1st ` p ) ) = N ) )
27 4 6 26 f1oresrab 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) : { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> { q e. ( WWalks ` G ) | ( # ` q ) = ( N + 1 ) } )
28 1 mpteq1i 
 |-  ( t e. T |-> ( 2nd ` t ) ) = ( t e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` t ) )
29 ssrab2 
 |-  { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } C_ ( Walks ` G )
30 resmpt 
 |-  ( { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } C_ ( Walks ` G ) -> ( ( t e. ( Walks ` G ) |-> ( 2nd ` t ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) = ( t e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` t ) ) )
31 29 30 ax-mp 
 |-  ( ( t e. ( Walks ` G ) |-> ( 2nd ` t ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) = ( t e. { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } |-> ( 2nd ` t ) )
32 fveq2 
 |-  ( t = p -> ( 2nd ` t ) = ( 2nd ` p ) )
33 32 cbvmptv 
 |-  ( t e. ( Walks ` G ) |-> ( 2nd ` t ) ) = ( p e. ( Walks ` G ) |-> ( 2nd ` p ) )
34 33 reseq1i 
 |-  ( ( t e. ( Walks ` G ) |-> ( 2nd ` t ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) = ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } )
35 28 31 34 3eqtr2i 
 |-  ( t e. T |-> ( 2nd ` t ) ) = ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } )
36 35 a1i 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( t e. T |-> ( 2nd ` t ) ) = ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) )
37 3 36 syl5eq 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> F = ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) )
38 1 a1i 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> T = { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } )
39 wwlksn 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { q e. ( WWalks ` G ) | ( # ` q ) = ( N + 1 ) } )
40 39 adantl 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( N WWalksN G ) = { q e. ( WWalks ` G ) | ( # ` q ) = ( N + 1 ) } )
41 2 40 syl5eq 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> W = { q e. ( WWalks ` G ) | ( # ` q ) = ( N + 1 ) } )
42 37 38 41 f1oeq123d 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> ( F : T -1-1-onto-> W <-> ( ( p e. ( Walks ` G ) |-> ( 2nd ` p ) ) |` { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) : { p e. ( Walks ` G ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> { q e. ( WWalks ` G ) | ( # ` q ) = ( N + 1 ) } ) )
43 27 42 mpbird 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> F : T -1-1-onto-> W )