Metamath Proof Explorer

Theorem clwwlkvbij

Description: There is a bijection between the set of closed walks of a fixed length N on a fixed vertex X represented by walks (as word) and the set of closed walks (as words) of the fixed length N on the fixed vertex X . The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 7-Jul-2022) (Proof shortened by AV, 2-Nov-2022)

Ref Expression
Assertion clwwlkvbij 
|- ( ( X e. V /\ N e. NN ) -> E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( N WWalksN G ) e. _V
2 1 mptrabex 
 |-  ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) e. _V
3 2 resex 
 |-  ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) e. _V
4 eqid 
 |-  ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) = ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) )
5 eqid 
 |-  { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } = { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) }
6 5 4 clwwlkf1o 
 |-  ( N e. NN -> ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) : { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } -1-1-onto-> ( N ClWWalksN G ) )
7 fveq1 
 |-  ( y = ( w prefix N ) -> ( y ` 0 ) = ( ( w prefix N ) ` 0 ) )
8 7 eqeq1d 
 |-  ( y = ( w prefix N ) -> ( ( y ` 0 ) = X <-> ( ( w prefix N ) ` 0 ) = X ) )
9 8 3ad2ant3 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ y = ( w prefix N ) ) -> ( ( y ` 0 ) = X <-> ( ( w prefix N ) ` 0 ) = X ) )
10 fveq2 
 |-  ( x = w -> ( lastS ` x ) = ( lastS ` w ) )
11 fveq1 
 |-  ( x = w -> ( x ` 0 ) = ( w ` 0 ) )
12 10 11 eqeq12d 
 |-  ( x = w -> ( ( lastS ` x ) = ( x ` 0 ) <-> ( lastS ` w ) = ( w ` 0 ) ) )
13 12 elrab 
 |-  ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } <-> ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) )
14 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
15 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
16 14 15 wwlknp 
 |-  ( w e. ( N WWalksN G ) -> ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
17 simpll 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) /\ N e. NN ) -> w e. Word ( Vtx ` G ) )
18 nnz 
 |-  ( N e. NN -> N e. ZZ )
19 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
20 peano2uz 
 |-  ( N e. ( ZZ>= ` N ) -> ( N + 1 ) e. ( ZZ>= ` N ) )
21 18 19 20 3syl 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` N ) )
22 elfz1end 
 |-  ( N e. NN <-> N e. ( 1 ... N ) )
23 22 biimpi 
 |-  ( N e. NN -> N e. ( 1 ... N ) )
24 fzss2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( N + 1 ) ) )
25 24 sselda 
 |-  ( ( ( N + 1 ) e. ( ZZ>= ` N ) /\ N e. ( 1 ... N ) ) -> N e. ( 1 ... ( N + 1 ) ) )
26 21 23 25 syl2anc 
 |-  ( N e. NN -> N e. ( 1 ... ( N + 1 ) ) )
27 26 adantl 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) /\ N e. NN ) -> N e. ( 1 ... ( N + 1 ) ) )
28 oveq2 
 |-  ( ( # ` w ) = ( N + 1 ) -> ( 1 ... ( # ` w ) ) = ( 1 ... ( N + 1 ) ) )
29 28 eleq2d 
 |-  ( ( # ` w ) = ( N + 1 ) -> ( N e. ( 1 ... ( # ` w ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
30 29 adantl 
 |-  ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) -> ( N e. ( 1 ... ( # ` w ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
31 30 adantr 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) /\ N e. NN ) -> ( N e. ( 1 ... ( # ` w ) ) <-> N e. ( 1 ... ( N + 1 ) ) ) )
32 27 31 mpbird 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) /\ N e. NN ) -> N e. ( 1 ... ( # ` w ) ) )
33 17 32 jca 
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) /\ N e. NN ) -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) )
34 33 ex 
 |-  ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) -> ( N e. NN -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) ) )
35 34 3adant3 
 |-  ( ( w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( N e. NN -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) ) )
36 16 35 syl 
 |-  ( w e. ( N WWalksN G ) -> ( N e. NN -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) ) )
37 36 adantr 
 |-  ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) -> ( N e. NN -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) ) )
38 13 37 sylbi 
 |-  ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } -> ( N e. NN -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) ) )
39 38 impcom 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } ) -> ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) )
40 pfxfv0 
 |-  ( ( w e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` w ) ) ) -> ( ( w prefix N ) ` 0 ) = ( w ` 0 ) )
41 39 40 syl 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } ) -> ( ( w prefix N ) ` 0 ) = ( w ` 0 ) )
42 41 eqeq1d 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } ) -> ( ( ( w prefix N ) ` 0 ) = X <-> ( w ` 0 ) = X ) )
43 42 3adant3 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ y = ( w prefix N ) ) -> ( ( ( w prefix N ) ` 0 ) = X <-> ( w ` 0 ) = X ) )
44 9 43 bitrd 
 |-  ( ( N e. NN /\ w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ y = ( w prefix N ) ) -> ( ( y ` 0 ) = X <-> ( w ` 0 ) = X ) )
45 4 6 44 f1oresrab 
 |-  ( N e. NN -> ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> { y e. ( N ClWWalksN G ) | ( y ` 0 ) = X } )
46 45 adantl 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> { y e. ( N ClWWalksN G ) | ( y ` 0 ) = X } )
47 clwwlknon 
 |-  ( X ( ClWWalksNOn ` G ) N ) = { y e. ( N ClWWalksN G ) | ( y ` 0 ) = X }
48 47 a1i 
 |-  ( ( X e. V /\ N e. NN ) -> ( X ( ClWWalksNOn ` G ) N ) = { y e. ( N ClWWalksN G ) | ( y ` 0 ) = X } )
49 48 f1oeq3d 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> { y e. ( N ClWWalksN G ) | ( y ` 0 ) = X } ) )
50 46 49 mpbird 
 |-  ( ( X e. V /\ N e. NN ) -> ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
51 f1oeq1 
 |-  ( f = ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) -> ( f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) )
52 51 spcegv 
 |-  ( ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) e. _V -> ( ( ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } |-> ( w prefix N ) ) |` { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } ) : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) -> E. f f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) )
53 3 50 52 mpsyl 
 |-  ( ( X e. V /\ N e. NN ) -> E. f f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
54 df-rab 
 |-  { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } = { w | ( w e. ( N WWalksN G ) /\ ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) }
55 anass 
 |-  ( ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) <-> ( w e. ( N WWalksN G ) /\ ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) )
56 55 bicomi 
 |-  ( ( w e. ( N WWalksN G ) /\ ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) <-> ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) )
57 56 abbii 
 |-  { w | ( w e. ( N WWalksN G ) /\ ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) ) } = { w | ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) }
58 13 bicomi 
 |-  ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) <-> w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } )
59 58 anbi1i 
 |-  ( ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) <-> ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ ( w ` 0 ) = X ) )
60 59 abbii 
 |-  { w | ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) } = { w | ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ ( w ` 0 ) = X ) }
61 df-rab 
 |-  { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } = { w | ( w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } /\ ( w ` 0 ) = X ) }
62 60 61 eqtr4i 
 |-  { w | ( ( w e. ( N WWalksN G ) /\ ( lastS ` w ) = ( w ` 0 ) ) /\ ( w ` 0 ) = X ) } = { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X }
63 54 57 62 3eqtri 
 |-  { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } = { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X }
64 f1oeq2 
 |-  ( { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } = { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -> ( f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) )
65 63 64 mp1i 
 |-  ( ( X e. V /\ N e. NN ) -> ( f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) )
66 65 exbidv 
 |-  ( ( X e. V /\ N e. NN ) -> ( E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) <-> E. f f : { w e. { x e. ( N WWalksN G ) | ( lastS ` x ) = ( x ` 0 ) } | ( w ` 0 ) = X } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) )
67 53 66 mpbird 
 |-  ( ( X e. V /\ N e. NN ) -> E. f f : { w e. ( N WWalksN G ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )