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

Metamath Proof Explorer

Theorem wwlksnextbij0

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021)

Ref Expression
Hypotheses wwlksnextbij0.v 
|- V = ( Vtx ` G )
wwlksnextbij0.e 
|- E = ( Edg ` G )
wwlksnextbij0.d 
|- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
wwlksnextbij0.r 
|- R = { n e. V | { ( lastS ` W ) , n } e. E }
wwlksnextbij0.f 
|- F = ( t e. D |-> ( lastS ` t ) )
Assertion wwlksnextbij0 
|- ( W e. ( N WWalksN G ) -> F : D -1-1-onto-> R )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v 
 |-  V = ( Vtx ` G )
2 wwlksnextbij0.e 
 |-  E = ( Edg ` G )
3 wwlksnextbij0.d 
 |-  D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
4 wwlksnextbij0.r 
 |-  R = { n e. V | { ( lastS ` W ) , n } e. E }
5 wwlksnextbij0.f 
 |-  F = ( t e. D |-> ( lastS ` t ) )
6 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
7 1 2 3 4 5 wwlksnextinj 
 |-  ( N e. NN0 -> F : D -1-1-> R )
8 7 3ad2ant2 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> F : D -1-1-> R )
9 6 8 syl 
 |-  ( W e. ( N WWalksN G ) -> F : D -1-1-> R )
10 1 2 3 4 5 wwlksnextsurj 
 |-  ( W e. ( N WWalksN G ) -> F : D -onto-> R )
11 df-f1o 
 |-  ( F : D -1-1-onto-> R <-> ( F : D -1-1-> R /\ F : D -onto-> R ) )
12 9 10 11 sylanbrc 
 |-  ( W e. ( N WWalksN G ) -> F : D -1-1-onto-> R )