Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlk.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
numclwwlk.q |
⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } ) |
3 |
|
numclwwlk.h |
⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) |
4 |
|
ovexd |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ∈ V ) |
5 |
|
eqid |
⊢ ( ℎ ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( ℎ prefix ( 𝑁 + 1 ) ) ) = ( ℎ ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( ℎ prefix ( 𝑁 + 1 ) ) ) |
6 |
1 2 3 5
|
numclwlk2lem2f1o |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ℎ ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( ℎ prefix ( 𝑁 + 1 ) ) ) : ( 𝑋 𝐻 ( 𝑁 + 2 ) ) –1-1-onto→ ( 𝑋 𝑄 𝑁 ) ) |
7 |
4 6
|
hasheqf1od |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) = ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) ) |
8 |
7
|
eqcomd |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝑄 𝑁 ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) ) |