Metamath Proof Explorer

Theorem clwwlknonclwlknonf1o

Description: F is a bijection between the two representations of closed walks of a fixed positive length on a fixed vertex. (Contributed by AV, 26-May-2022) (Proof shortened by AV, 7-Aug-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlknonclwlknonf1o.v 
|- V = ( Vtx ` G )
clwwlknonclwlknonf1o.w 
|- W = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) }
clwwlknonclwlknonf1o.f 
|- F = ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
Assertion clwwlknonclwlknonf1o 
|- ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> F : W -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )

Proof

Step Hyp Ref Expression
1 clwwlknonclwlknonf1o.v 
 |-  V = ( Vtx ` G )
2 clwwlknonclwlknonf1o.w 
 |-  W = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) }
3 clwwlknonclwlknonf1o.f 
 |-  F = ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
4 eqid 
 |-  { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N }
5 eqid 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) = ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
6 eqid 
 |-  ( 1st ` c ) = ( 1st ` c )
7 eqid 
 |-  ( 2nd ` c ) = ( 2nd ` c )
8 6 7 4 5 clwlknf1oclwwlkn 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } -1-1-onto-> ( N ClWWalksN G ) )
9 8 3adant2 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } -1-1-onto-> ( N ClWWalksN G ) )
10 fveq1 
 |-  ( s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) -> ( s ` 0 ) = ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` 0 ) )
11 10 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } /\ s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( s ` 0 ) = ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` 0 ) )
12 2fveq3 
 |-  ( w = c -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` c ) ) )
13 12 eqeq1d 
 |-  ( w = c -> ( ( # ` ( 1st ` w ) ) = N <-> ( # ` ( 1st ` c ) ) = N ) )
14 13 elrab 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } <-> ( c e. ( ClWalks ` G ) /\ ( # ` ( 1st ` c ) ) = N ) )
15 clwlkwlk 
 |-  ( c e. ( ClWalks ` G ) -> c e. ( Walks ` G ) )
16 wlkcpr 
 |-  ( c e. ( Walks ` G ) <-> ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) )
17 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
18 17 wlkpwrd 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( 2nd ` c ) e. Word ( Vtx ` G ) )
19 18 3ad2ant1 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( 2nd ` c ) e. Word ( Vtx ` G ) )
20 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
21 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
22 20 21 sylbi 
 |-  ( N e. NN -> N e. ( 1 ... N ) )
23 fzelp1 
 |-  ( N e. ( 1 ... N ) -> N e. ( 1 ... ( N + 1 ) ) )
24 22 23 syl 
 |-  ( N e. NN -> N e. ( 1 ... ( N + 1 ) ) )
25 24 3ad2ant3 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> N e. ( 1 ... ( N + 1 ) ) )
26 25 3ad2ant3 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> N e. ( 1 ... ( N + 1 ) ) )
27 id 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( # ` ( 1st ` c ) ) = N )
28 oveq1 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( ( # ` ( 1st ` c ) ) + 1 ) = ( N + 1 ) )
29 28 oveq2d 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) = ( 1 ... ( N + 1 ) ) )
30 27 29 eleq12d 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( ( # ` ( 1st ` c ) ) e. ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
31 30 3ad2ant2 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( ( # ` ( 1st ` c ) ) e. ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
32 26 31 mpbird 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( # ` ( 1st ` c ) ) e. ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) )
33 wlklenvp1 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( # ` ( 2nd ` c ) ) = ( ( # ` ( 1st ` c ) ) + 1 ) )
34 33 oveq2d 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( 1 ... ( # ` ( 2nd ` c ) ) ) = ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) )
35 34 eleq2d 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) <-> ( # ` ( 1st ` c ) ) e. ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) ) )
36 35 3ad2ant1 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) <-> ( # ` ( 1st ` c ) ) e. ( 1 ... ( ( # ` ( 1st ` c ) ) + 1 ) ) ) )
37 32 36 mpbird 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) )
38 19 37 jca 
 |-  ( ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) /\ ( # ` ( 1st ` c ) ) = N /\ ( G e. USPGraph /\ X e. V /\ N e. NN ) ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) )
39 38 3exp 
 |-  ( ( 1st ` c ) ( Walks ` G ) ( 2nd ` c ) -> ( ( # ` ( 1st ` c ) ) = N -> ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) ) ) )
40 16 39 sylbi 
 |-  ( c e. ( Walks ` G ) -> ( ( # ` ( 1st ` c ) ) = N -> ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) ) ) )
41 15 40 syl 
 |-  ( c e. ( ClWalks ` G ) -> ( ( # ` ( 1st ` c ) ) = N -> ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) ) ) )
42 41 imp 
 |-  ( ( c e. ( ClWalks ` G ) /\ ( # ` ( 1st ` c ) ) = N ) -> ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) ) )
43 14 42 sylbi 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } -> ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) ) )
44 43 impcom 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } ) -> ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) )
45 pfxfv0 
 |-  ( ( ( 2nd ` c ) e. Word ( Vtx ` G ) /\ ( # ` ( 1st ` c ) ) e. ( 1 ... ( # ` ( 2nd ` c ) ) ) ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
46 44 45 syl 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
47 46 3adant3 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } /\ s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
48 11 47 eqtrd 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } /\ s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( s ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
49 48 eqeq1d 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } /\ s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( s ` 0 ) = X <-> ( ( 2nd ` c ) ` 0 ) = X ) )
50 nfv 
 |-  F/ w ( ( 2nd ` c ) ` 0 ) = X
51 fveq2 
 |-  ( w = c -> ( 2nd ` w ) = ( 2nd ` c ) )
52 51 fveq1d 
 |-  ( w = c -> ( ( 2nd ` w ) ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
53 52 eqeq1d 
 |-  ( w = c -> ( ( ( 2nd ` w ) ` 0 ) = X <-> ( ( 2nd ` c ) ` 0 ) = X ) )
54 50 53 sbiev 
 |-  ( [ c / w ] ( ( 2nd ` w ) ` 0 ) = X <-> ( ( 2nd ` c ) ` 0 ) = X )
55 49 54 bitr4di 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. NN ) /\ c e. { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } /\ s = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( s ` 0 ) = X <-> [ c / w ] ( ( 2nd ` w ) ` 0 ) = X ) )
56 2 4 3 5 9 55 f1ossf1o 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> F : W -1-1-onto-> { s e. ( N ClWWalksN G ) | ( s ` 0 ) = X } )
57 clwwlknon 
 |-  ( X ( ClWWalksNOn ` G ) N ) = { s e. ( N ClWWalksN G ) | ( s ` 0 ) = X }
58 f1oeq3 
 |-  ( ( X ( ClWWalksNOn ` G ) N ) = { s e. ( N ClWWalksN G ) | ( s ` 0 ) = X } -> ( F : W -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> F : W -1-1-onto-> { s e. ( N ClWWalksN G ) | ( s ` 0 ) = X } ) )
59 57 58 ax-mp 
 |-  ( F : W -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> F : W -1-1-onto-> { s e. ( N ClWWalksN G ) | ( s ` 0 ) = X } )
60 56 59 sylibr 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> F : W -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )