Theorem rusgrnumwwlklem

Description: Lemma for rusgrnumwwlk etc. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	rusgrnumwwlk.l	⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
Assertion	rusgrnumwwlklem	⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 𝐿 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		rusgrnumwwlk.l	⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
3		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 ) )
4	3	adantl	⊢ ( ( 𝑣 = 𝑃 ∧ 𝑛 = 𝑁 ) → ( 𝑛 WWalksN 𝐺 ) = ( 𝑁 WWalksN 𝐺 ) )
5		eqeq2	⊢ ( 𝑣 = 𝑃 → ( ( 𝑤 ‘ 0 ) = 𝑣 ↔ ( 𝑤 ‘ 0 ) = 𝑃 ) )
6	5	adantr	⊢ ( ( 𝑣 = 𝑃 ∧ 𝑛 = 𝑁 ) → ( ( 𝑤 ‘ 0 ) = 𝑣 ↔ ( 𝑤 ‘ 0 ) = 𝑃 ) )
7	4 6	rabeqbidv	⊢ ( ( 𝑣 = 𝑃 ∧ 𝑛 = 𝑁 ) → { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } )
8	7	fveq2d	⊢ ( ( 𝑣 = 𝑃 ∧ 𝑛 = 𝑁 ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
9		fvex	⊢ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) ∈ V
10	8 2 9	ovmpoa	⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 𝐿 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )