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