Metamath Proof Explorer

Theorem wwlksnextbij

Description: There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij.v 
|- V = ( Vtx ` G )
wwlksnextbij.e 
|- E = ( Edg ` G )
Assertion wwlksnextbij 
|- ( W e. ( N WWalksN G ) -> E. f f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )

Proof

Step Hyp Ref Expression
1 wwlksnextbij.v 
 |-  V = ( Vtx ` G )
2 wwlksnextbij.e 
 |-  E = ( Edg ` G )
3 ovexd 
 |-  ( W e. ( N WWalksN G ) -> ( ( N + 1 ) WWalksN G ) e. _V )
4 rabexg 
 |-  ( ( ( N + 1 ) WWalksN G ) e. _V -> { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } e. _V )
5 mptexg 
 |-  ( { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } e. _V -> ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) e. _V )
6 3 4 5 3syl 
 |-  ( W e. ( N WWalksN G ) -> ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) e. _V )
7 eqid 
 |-  { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
8 preq2 
 |-  ( n = p -> { ( lastS ` W ) , n } = { ( lastS ` W ) , p } )
9 8 eleq1d 
 |-  ( n = p -> ( { ( lastS ` W ) , n } e. E <-> { ( lastS ` W ) , p } e. E ) )
10 9 cbvrabv 
 |-  { n e. V | { ( lastS ` W ) , n } e. E } = { p e. V | { ( lastS ` W ) , p } e. E }
11 fveqeq2 
 |-  ( t = w -> ( ( # ` t ) = ( N + 2 ) <-> ( # ` w ) = ( N + 2 ) ) )
12 oveq1 
 |-  ( t = w -> ( t prefix ( N + 1 ) ) = ( w prefix ( N + 1 ) ) )
13 12 eqeq1d 
 |-  ( t = w -> ( ( t prefix ( N + 1 ) ) = W <-> ( w prefix ( N + 1 ) ) = W ) )
14 fveq2 
 |-  ( t = w -> ( lastS ` t ) = ( lastS ` w ) )
15 14 preq2d 
 |-  ( t = w -> { ( lastS ` W ) , ( lastS ` t ) } = { ( lastS ` W ) , ( lastS ` w ) } )
16 15 eleq1d 
 |-  ( t = w -> ( { ( lastS ` W ) , ( lastS ` t ) } e. E <-> { ( lastS ` W ) , ( lastS ` w ) } e. E ) )
17 11 13 16 3anbi123d 
 |-  ( t = w -> ( ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) <-> ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) )
18 17 cbvrabv 
 |-  { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
19 18 mpteq1i 
 |-  ( x e. { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) = ( x e. { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } |-> ( lastS ` x ) )
20 1 2 7 10 19 wwlksnextbij0 
 |-  ( W e. ( N WWalksN G ) -> ( x e. { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) : { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )
21 eqid 
 |-  { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } = { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) }
22 1 2 21 wwlksnextwrd 
 |-  ( W e. ( N WWalksN G ) -> { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } = { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } )
23 22 eqcomd 
 |-  ( W e. ( N WWalksN G ) -> { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } = { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } )
24 23 mpteq1d 
 |-  ( W e. ( N WWalksN G ) -> ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) = ( x e. { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) )
25 1 2 7 wwlksnextwrd 
 |-  ( W e. ( N WWalksN G ) -> { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
26 25 eqcomd 
 |-  ( W e. ( N WWalksN G ) -> { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
27 eqidd 
 |-  ( W e. ( N WWalksN G ) -> { n e. V | { ( lastS ` W ) , n } e. E } = { n e. V | { ( lastS ` W ) , n } e. E } )
28 24 26 27 f1oeq123d 
 |-  ( W e. ( N WWalksN G ) -> ( ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } <-> ( x e. { t e. Word V | ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) : { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } ) )
29 20 28 mpbird 
 |-  ( W e. ( N WWalksN G ) -> ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )
30 f1oeq1 
 |-  ( f = ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) -> ( f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } <-> ( x e. { t e. ( ( N + 1 ) WWalksN G ) | ( ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) } |-> ( lastS ` x ) ) : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } ) )
31 6 29 30 spcedv 
 |-  ( W e. ( N WWalksN G ) -> E. f f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )