Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1o

Description: F is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022) (Revised by AV, 1-Nov-2022)

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

Proof

Step Hyp Ref Expression
1 dlwwlknondlwlknonbij.v 
 |-  V = ( Vtx ` G )
2 dlwwlknondlwlknonbij.w 
 |-  W = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
3 dlwwlknondlwlknonbij.d 
 |-  D = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X }
4 dlwwlknondlwlknonf1o.f 
 |-  F = ( c e. W |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
5 df-3an 
 |-  ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) <-> ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) )
6 5 rabbii 
 |-  { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) } = { w e. ( ClWalks ` G ) | ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
7 2 6 eqtri 
 |-  W = { w e. ( ClWalks ` G ) | ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
8 eqid 
 |-  { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) }
9 eqid 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) = ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
10 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
11 1 8 9 clwwlknonclwlknonf1o 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
12 10 11 syl3an3 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
13 fveq1 
 |-  ( y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) -> ( y ` ( N - 2 ) ) = ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` ( N - 2 ) ) )
14 13 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } /\ y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( y ` ( N - 2 ) ) = ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` ( N - 2 ) ) )
15 2fveq3 
 |-  ( w = c -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` c ) ) )
16 15 eqeq1d 
 |-  ( w = c -> ( ( # ` ( 1st ` w ) ) = N <-> ( # ` ( 1st ` c ) ) = N ) )
17 fveq2 
 |-  ( w = c -> ( 2nd ` w ) = ( 2nd ` c ) )
18 17 fveq1d 
 |-  ( w = c -> ( ( 2nd ` w ) ` 0 ) = ( ( 2nd ` c ) ` 0 ) )
19 18 eqeq1d 
 |-  ( w = c -> ( ( ( 2nd ` w ) ` 0 ) = X <-> ( ( 2nd ` c ) ` 0 ) = X ) )
20 16 19 anbi12d 
 |-  ( w = c -> ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) )
21 20 elrab 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } <-> ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) )
22 simplrl 
 |-  ( ( ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) /\ ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( # ` ( 1st ` c ) ) = N )
23 simpll 
 |-  ( ( ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) /\ ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> c e. ( ClWalks ` G ) )
24 simpr3 
 |-  ( ( ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) /\ ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> N e. ( ZZ>= ` 2 ) )
25 22 23 24 3jca 
 |-  ( ( ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) /\ ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( ( # ` ( 1st ` c ) ) = N /\ c e. ( ClWalks ` G ) /\ N e. ( ZZ>= ` 2 ) ) )
26 25 ex 
 |-  ( ( c e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` c ) ) = N /\ ( ( 2nd ` c ) ` 0 ) = X ) ) -> ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( 1st ` c ) ) = N /\ c e. ( ClWalks ` G ) /\ N e. ( ZZ>= ` 2 ) ) ) )
27 21 26 sylbi 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } -> ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( 1st ` c ) ) = N /\ c e. ( ClWalks ` G ) /\ N e. ( ZZ>= ` 2 ) ) ) )
28 27 impcom 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) -> ( ( # ` ( 1st ` c ) ) = N /\ c e. ( ClWalks ` G ) /\ N e. ( ZZ>= ` 2 ) ) )
29 dlwwlknondlwlknonf1olem1 
 |-  ( ( ( # ` ( 1st ` c ) ) = N /\ c e. ( ClWalks ` G ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` ( N - 2 ) ) = ( ( 2nd ` c ) ` ( N - 2 ) ) )
30 28 29 syl 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` ( N - 2 ) ) = ( ( 2nd ` c ) ` ( N - 2 ) ) )
31 30 3adant3 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } /\ y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ` ( N - 2 ) ) = ( ( 2nd ` c ) ` ( N - 2 ) ) )
32 14 31 eqtrd 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } /\ y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( y ` ( N - 2 ) ) = ( ( 2nd ` c ) ` ( N - 2 ) ) )
33 32 eqeq1d 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } /\ y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( y ` ( N - 2 ) ) = X <-> ( ( 2nd ` c ) ` ( N - 2 ) ) = X ) )
34 nfv 
 |-  F/ w ( ( 2nd ` c ) ` ( N - 2 ) ) = X
35 17 fveq1d 
 |-  ( w = c -> ( ( 2nd ` w ) ` ( N - 2 ) ) = ( ( 2nd ` c ) ` ( N - 2 ) ) )
36 35 eqeq1d 
 |-  ( w = c -> ( ( ( 2nd ` w ) ` ( N - 2 ) ) = X <-> ( ( 2nd ` c ) ` ( N - 2 ) ) = X ) )
37 34 36 sbiev 
 |-  ( [ c / w ] ( ( 2nd ` w ) ` ( N - 2 ) ) = X <-> ( ( 2nd ` c ) ` ( N - 2 ) ) = X )
38 33 37 bitr4di 
 |-  ( ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) /\ c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } /\ y = ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) -> ( ( y ` ( N - 2 ) ) = X <-> [ c / w ] ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) )
39 7 8 4 9 12 38 f1ossf1o 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> F : W -1-1-onto-> { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X } )
40 fveq1 
 |-  ( w = y -> ( w ` ( N - 2 ) ) = ( y ` ( N - 2 ) ) )
41 40 eqeq1d 
 |-  ( w = y -> ( ( w ` ( N - 2 ) ) = X <-> ( y ` ( N - 2 ) ) = X ) )
42 41 cbvrabv 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } = { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X }
43 3 42 eqtri 
 |-  D = { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X }
44 f1oeq3 
 |-  ( D = { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X } -> ( F : W -1-1-onto-> D <-> F : W -1-1-onto-> { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X } ) )
45 43 44 ax-mp 
 |-  ( F : W -1-1-onto-> D <-> F : W -1-1-onto-> { y e. ( X ( ClWWalksNOn ` G ) N ) | ( y ` ( N - 2 ) ) = X } )
46 39 45 sylibr 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> F : W -1-1-onto-> D )