Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlknonfin.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
clwwlknon |
⊢ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } |
3 |
1
|
eleq1i |
⊢ ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin ) |
4 |
|
clwwlknfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin ) |
5 |
3 4
|
sylbi |
⊢ ( 𝑉 ∈ Fin → ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin ) |
6 |
|
rabfi |
⊢ ( ( 𝑁 ClWWalksN 𝐺 ) ∈ Fin → { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin ) |
7 |
5 6
|
syl |
⊢ ( 𝑉 ∈ Fin → { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑋 } ∈ Fin ) |
8 |
2 7
|
eqeltrid |
⊢ ( 𝑉 ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin ) |