Metamath Proof Explorer


Theorem wlkiswwlks2

Description: A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Assertion wlkiswwlks2 ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wwlkbp ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) )
3 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 1 3 iswwlks ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
5 ovex ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ V
6 mptexg ( ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ V → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ V )
7 5 6 mp1i ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ V )
8 simprr ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → 𝐺 ∈ USPGraph )
9 simplr ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
10 hashge1 ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝑃 ) )
11 10 ancoms ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → 1 ≤ ( ♯ ‘ 𝑃 ) )
12 11 adantr ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → 1 ≤ ( ♯ ‘ 𝑃 ) )
13 8 9 12 3jca ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
14 13 adantr ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
15 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
16 15 a1i ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
17 16 eleq2d ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) ) )
18 17 ralbidv ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) ) )
19 18 biimpd ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) ) )
20 eqid ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
21 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
22 20 21 wlkiswwlks2lem6 ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran ( iEdg ‘ 𝐺 ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
23 14 19 22 sylsyld ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
24 eleq1 ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) )
25 fveq2 ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) )
26 25 oveq2d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) )
27 26 feq2d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
28 25 oveq2d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) )
29 fveq1 ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( 𝑓𝑖 ) = ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) )
30 29 fveqeq2d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
31 28 30 raleqbidv ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
32 24 27 31 3anbi123d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
33 32 imbi2d ( 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
34 33 adantl ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ‘ 𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
35 23 34 mpbird ( ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝑓 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ( iEdg ‘ 𝐺 ) ‘ { ( 𝑃𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
36 7 35 spcimedv ( ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
37 36 ex ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
38 37 com23 ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
39 38 3impia ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ USPGraph ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
40 39 expd ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) )
41 40 impcom ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
42 41 imp ( ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝐺 ∈ USPGraph ) → ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
43 uspgrupgr ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
44 1 21 upgriswlk ( 𝐺 ∈ UPGraph → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
45 43 44 syl ( 𝐺 ∈ USPGraph → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
46 45 adantl ( ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝐺 ∈ USPGraph ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
47 46 exbidv ( ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝐺 ∈ USPGraph ) → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ↔ ∃ 𝑓 ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
48 42 47 mpbird ( ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝐺 ∈ USPGraph ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 )
49 48 ex ( ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
50 49 ex ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) ) )
51 4 50 syl5bi ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) ) )
52 2 51 mpcom ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ USPGraph → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
53 52 com12 ( 𝐺 ∈ USPGraph → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )