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

Metamath Proof Explorer

Theorem clwlknf1oclwwlkn

Description: There is a one-to-one onto function between the set of closed walks as words of length N and the set of closed walks of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a 
|- A = ( 1st ` c )
clwlknf1oclwwlkn.b 
|- B = ( 2nd ` c )
clwlknf1oclwwlkn.c 
|- C = { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N }
clwlknf1oclwwlkn.f 
|- F = ( c e. C |-> ( B prefix ( # ` A ) ) )
Assertion clwlknf1oclwwlkn 
|- ( ( G e. USPGraph /\ N e. NN ) -> F : C -1-1-onto-> ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a 
 |-  A = ( 1st ` c )
2 clwlknf1oclwwlkn.b 
 |-  B = ( 2nd ` c )
3 clwlknf1oclwwlkn.c 
 |-  C = { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N }
4 clwlknf1oclwwlkn.f 
 |-  F = ( c e. C |-> ( B prefix ( # ` A ) ) )
5 eqid 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
6 2fveq3 
 |-  ( s = w -> ( # ` ( 1st ` s ) ) = ( # ` ( 1st ` w ) ) )
7 6 breq2d 
 |-  ( s = w -> ( 1 <_ ( # ` ( 1st ` s ) ) <-> 1 <_ ( # ` ( 1st ` w ) ) ) )
8 7 cbvrabv 
 |-  { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
9 fveq2 
 |-  ( d = c -> ( 2nd ` d ) = ( 2nd ` c ) )
10 2fveq3 
 |-  ( d = c -> ( # ` ( 2nd ` d ) ) = ( # ` ( 2nd ` c ) ) )
11 10 oveq1d 
 |-  ( d = c -> ( ( # ` ( 2nd ` d ) ) - 1 ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
12 9 11 oveq12d 
 |-  ( d = c -> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
13 12 cbvmptv 
 |-  ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) = ( c e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
14 8 13 clwlkclwwlkf1o 
 |-  ( G e. USPGraph -> ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) : { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } -1-1-onto-> ( ClWWalks ` G ) )
15 14 adantr 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) : { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } -1-1-onto-> ( ClWWalks ` G ) )
16 2fveq3 
 |-  ( w = s -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` s ) ) )
17 16 breq2d 
 |-  ( w = s -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ ( # ` ( 1st ` s ) ) ) )
18 17 cbvrabv 
 |-  { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } = { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) }
19 18 mpteq1i 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( c e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
20 fveq2 
 |-  ( c = d -> ( 2nd ` c ) = ( 2nd ` d ) )
21 2fveq3 
 |-  ( c = d -> ( # ` ( 2nd ` c ) ) = ( # ` ( 2nd ` d ) ) )
22 21 oveq1d 
 |-  ( c = d -> ( ( # ` ( 2nd ` c ) ) - 1 ) = ( ( # ` ( 2nd ` d ) ) - 1 ) )
23 20 22 oveq12d 
 |-  ( c = d -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) = ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) )
24 23 cbvmptv 
 |-  ( c e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) )
25 19 24 eqtri 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) )
26 25 a1i 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) )
27 8 eqcomi 
 |-  { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } = { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) }
28 27 a1i 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } = { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } )
29 eqidd 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ClWWalks ` G ) = ( ClWWalks ` G ) )
30 26 28 29 f1oeq123d 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) : { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -1-1-onto-> ( ClWWalks ` G ) <-> ( d e. { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) : { s e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` s ) ) } -1-1-onto-> ( ClWWalks ` G ) ) )
31 15 30 mpbird 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) : { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -1-1-onto-> ( ClWWalks ` G ) )
32 fveq2 
 |-  ( s = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) -> ( # ` s ) = ( # ` ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) )
33 32 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ s = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) -> ( # ` s ) = ( # ` ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) )
34 2fveq3 
 |-  ( w = c -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` c ) ) )
35 34 breq2d 
 |-  ( w = c -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ ( # ` ( 1st ` c ) ) ) )
36 35 elrab 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } <-> ( c e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` c ) ) ) )
37 clwlknf1oclwwlknlem1 
 |-  ( ( c e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` c ) ) ) -> ( # ` ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( # ` ( 1st ` c ) ) )
38 36 37 sylbi 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -> ( # ` ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( # ` ( 1st ` c ) ) )
39 38 3ad2ant2 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ s = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) -> ( # ` ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) = ( # ` ( 1st ` c ) ) )
40 33 39 eqtrd 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ s = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) -> ( # ` s ) = ( # ` ( 1st ` c ) ) )
41 40 eqeq1d 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ s = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) -> ( ( # ` s ) = N <-> ( # ` ( 1st ` c ) ) = N ) )
42 5 31 41 f1oresrab 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) |` { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } ) : { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } -1-1-onto-> { s e. ( ClWWalks ` G ) | ( # ` s ) = N } )
43 1 2 3 4 clwlknf1oclwwlknlem3 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> F = ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) |` C ) )
44 2 a1i 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ) -> B = ( 2nd ` c ) )
45 clwlkwlk 
 |-  ( c e. ( ClWalks ` G ) -> c e. ( Walks ` G ) )
46 wlkcpr 
 |-  ( c e. ( Walks ` G ) <-> ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) )
47 1 fveq2i 
 |-  ( # ` A ) = ( # ` ( 1st ` c ) )
48 wlklenvm1 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( # ` ( 1st ` c ) ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
49 47 48 eqtrid 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
50 46 49 sylbi 
 |-  ( c e. ( Walks ` G ) -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
51 45 50 syl 
 |-  ( c e. ( ClWalks ` G ) -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
52 51 adantr 
 |-  ( ( c e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` c ) ) ) -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
53 36 52 sylbi 
 |-  ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
54 53 adantl 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ) -> ( # ` A ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
55 44 54 oveq12d 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ) -> ( B prefix ( # ` A ) ) = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
56 55 mpteq2dva 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) = ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) )
57 34 eqeq1d 
 |-  ( w = c -> ( ( # ` ( 1st ` w ) ) = N <-> ( # ` ( 1st ` c ) ) = N ) )
58 57 cbvrabv 
 |-  { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N }
59 nnge1 
 |-  ( N e. NN -> 1 <_ N )
60 breq2 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( 1 <_ ( # ` ( 1st ` c ) ) <-> 1 <_ N ) )
61 59 60 syl5ibrcom 
 |-  ( N e. NN -> ( ( # ` ( 1st ` c ) ) = N -> 1 <_ ( # ` ( 1st ` c ) ) ) )
62 61 adantl 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ( # ` ( 1st ` c ) ) = N -> 1 <_ ( # ` ( 1st ` c ) ) ) )
63 62 adantr 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. ( ClWalks ` G ) ) -> ( ( # ` ( 1st ` c ) ) = N -> 1 <_ ( # ` ( 1st ` c ) ) ) )
64 63 pm4.71rd 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ c e. ( ClWalks ` G ) ) -> ( ( # ` ( 1st ` c ) ) = N <-> ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) ) )
65 64 rabbidva 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )
66 58 65 eqtrid 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )
67 36 anbi1i 
 |-  ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ ( # ` ( 1st ` c ) ) = N ) <-> ( ( c e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) = N ) )
68 anass 
 |-  ( ( ( c e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` c ) ) ) /\ ( # ` ( 1st ` c ) ) = N ) <-> ( c e. ( ClWalks ` G ) /\ ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) ) )
69 67 68 bitri 
 |-  ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } /\ ( # ` ( 1st ` c ) ) = N ) <-> ( c e. ( ClWalks ` G ) /\ ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) ) )
70 69 rabbia2 
 |-  { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) }
71 66 3 70 3eqtr4g 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> C = { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } )
72 56 71 reseq12d 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) |` C ) = ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) |` { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } ) )
73 43 72 eqtrd 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> F = ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) |` { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } ) )
74 clwlknf1oclwwlknlem2 
 |-  ( N e. NN -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )
75 74 adantl 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )
76 75 3 70 3eqtr4g 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> C = { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } )
77 clwwlkn 
 |-  ( N ClWWalksN G ) = { s e. ( ClWWalks ` G ) | ( # ` s ) = N }
78 77 a1i 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( N ClWWalksN G ) = { s e. ( ClWWalks ` G ) | ( # ` s ) = N } )
79 73 76 78 f1oeq123d 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( F : C -1-1-onto-> ( N ClWWalksN G ) <-> ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) ) |` { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } ) : { c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } | ( # ` ( 1st ` c ) ) = N } -1-1-onto-> { s e. ( ClWWalks ` G ) | ( # ` s ) = N } ) )
80 42 79 mpbird 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> F : C -1-1-onto-> ( N ClWWalksN G ) )