Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnexthasheq.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wwlksnexthasheq.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
ovex |
⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∈ V |
4 |
3
|
rabex |
⊢ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∈ V |
5 |
1 2
|
wwlksnextbij |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ) |
6 |
|
hasheqf1oi |
⊢ ( { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ∈ V → ( ∃ 𝑓 𝑓 : { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ) = ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ) ) ) |
7 |
4 5 6
|
mpsyl |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑊 ∧ { ( lastS ‘ 𝑊 ) , ( lastS ‘ 𝑤 ) } ∈ 𝐸 ) } ) = ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑊 ) , 𝑛 } ∈ 𝐸 } ) ) |