Theorem numclwlk2lem2fv

Description: Value of the function R . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 31-May-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	numclwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	numclwwlk.q	⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
	numclwwlk.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
	numclwwlk.r	⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
Assertion	numclwlk2lem2fv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑊 ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		numclwwlk.q	⊢ 𝑄 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3		numclwwlk.h	⊢ 𝐻 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4		numclwwlk.r	⊢ 𝑅 = ( 𝑥 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ↦ ( 𝑥 prefix ( 𝑁 + 1 ) ) )
5		oveq1	⊢ ( 𝑥 = 𝑊 → ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) )
6		simpr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) )
7		ovexd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ V )
8	4 5 6 7	fvmptd3	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) ∧ 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) ) → ( 𝑅 ‘ 𝑊 ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) )
9	8	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑊 ∈ ( 𝑋 𝐻 ( 𝑁 + 2 ) ) → ( 𝑅 ‘ 𝑊 ) = ( 𝑊 prefix ( 𝑁 + 1 ) ) ) )