Theorem wwlknon

Description: An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

	Ref	Expression
Assertion	wwlknon	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
2	1	eqeq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 0 ) = 𝐴 ↔ ( 𝑊 ‘ 0 ) = 𝐴 ) )
3		fveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) )
4	3	eqeq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 𝑁 ) = 𝐵 ↔ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) )
5	2 4	anbi12d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) ↔ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) ) )
6		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7	6	iswwlksnon	⊢ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) }
8	5 7	elrab2	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) ) )
9		3anass	⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) ) )
10	8 9	bitr4i	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝐴 ∧ ( 𝑊 ‘ 𝑁 ) = 𝐵 ) )