Step |
Hyp |
Ref |
Expression |
1 |
|
fvex |
⊢ ( ClWalks ‘ 𝐺 ) ∈ V |
2 |
1
|
rabex |
⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ∈ V |
3 |
2
|
a1i |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ∈ V ) |
4 |
|
eqid |
⊢ ( 1st ‘ 𝑐 ) = ( 1st ‘ 𝑐 ) |
5 |
|
eqid |
⊢ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑐 ) |
6 |
|
eqid |
⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } |
7 |
|
eqid |
⊢ ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) |
8 |
4 5 6 7
|
clwlknf1oclwwlkn |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑐 ∈ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ↦ ( ( 2nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) ) : { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } –1-1-onto→ ( 𝑁 ClWWalksN 𝐺 ) ) |
9 |
3 8
|
hasheqf1od |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ) = ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) ) |
10 |
9
|
eqcomd |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 } ) ) |