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→ 𝑅 ) |