Metamath Proof Explorer


Theorem wksvOLD

Description: Obsolete version of wksv as of 11-Dec-2024. (Contributed by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion wksvOLD { ⟨ 𝑓 , 𝑝 ⟩ ∣ 𝑓 ( 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