Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlk3.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fusgrusgr |
⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph ) |
3 |
2
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → 𝐺 ∈ USGraph ) |
4 |
1
|
clwwlknun |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) |
7 |
1
|
fusgrvtxfi |
⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin ) |
8 |
7
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → 𝑉 ∈ Fin ) |
9 |
1
|
clwwlknonfin |
⊢ ( 𝑉 ∈ Fin → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin ) |
10 |
7 9
|
syl |
⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin ) |
11 |
10
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∈ Fin ) |
13 |
|
clwwlknondisj |
⊢ Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) |
14 |
13
|
a1i |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → Disj 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) |
15 |
8 12 14
|
hashiun |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) |
16 |
6 15
|
eqtrd |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) ) |