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 𝑉 = ( 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𝑅 )