Theorem wksv

Description: The class of walks is a set. (Contributed by AV, 15-Jan-2021)

	Ref	Expression
Assertion	wksv	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( Vtx ‘ 𝐺 ) ∈ V
2		fvex	⊢ ( iEdg ‘ 𝐺 ) ∈ V
3	2	dmex	⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
4		wrdexg	⊢ ( dom ( iEdg ‘ 𝐺 ) ∈ V → Word dom ( iEdg ‘ 𝐺 ) ∈ V )
5	3 4	mp1i	⊢ ( ( Vtx ‘ 𝐺 ) ∈ V → Word dom ( iEdg ‘ 𝐺 ) ∈ V )
6		wrdexg	⊢ ( ( Vtx ‘ 𝐺 ) ∈ V → Word ( Vtx ‘ 𝐺 ) ∈ V )
7		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8	7	wlkf	⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) )
9	8	adantl	⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) → 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) )
10		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11	10	wlkpwrd	⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) )
12	11	adantl	⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) → 𝑝 ∈ Word ( Vtx ‘ 𝐺 ) )
13	5 6 9 12	opabex2	⊢ ( ( Vtx ‘ 𝐺 ) ∈ V → { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V )
14	1 13	ax-mp	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V