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 )