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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wwlksnextbij0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	wwlksnextbij0.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
	wwlksnextbij0.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
	wwlksnextbij0.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
Assertion	wwlksnextbij0	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		wwlksnextbij0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wwlksnextbij0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		wwlksnextbij0.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 2 ) ∧ ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) }
4		wwlksnextbij0.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 }
5		wwlksnextbij0.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( lastS ‘ 𝑡 ) )
6	1	wwlknbp	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) )
7	1 2 3 4 5	wwlksnextinj	⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝐷 –1-1→ 𝑅 )
8	7	3ad2ant2	⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) → 𝐹 : 𝐷 –1-1→ 𝑅 )
9	6 8	syl	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –1-1→ 𝑅 )
10	1 2 3 4 5	wwlksnextsurj	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –onto→ 𝑅 )
11		df-f1o	⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝑅 ↔ ( 𝐹 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐷 –onto→ 𝑅 ) )
12	9 10 11	sylanbrc	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝐹 : 𝐷 –1-1-onto→ 𝑅 )