Metamath Proof Explorer


Theorem wlkiswwlks1

Description: The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 9-Apr-2021)

Ref Expression
Assertion wlkiswwlks1 ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 wlkn0 ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ≠ ∅ )
2 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 upgriswlk ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) )
5 simpr ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ≠ ∅ )
6 ffz0iswrd ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
7 6 3ad2ant2 ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
8 7 ad2antlr ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
9 upgruhgr ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
10 3 uhgrfun ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
11 funfn ( Fun ( iEdg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
12 11 biimpi ( Fun ( iEdg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
13 9 10 12 3syl ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
14 13 ad2antlr ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
15 wrdsymbcl ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) )
16 15 ad4ant14 ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) )
17 fnfvelrn ( ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) ∈ ran ( iEdg ‘ 𝐺 ) )
18 14 16 17 syl2anc ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) ∈ ran ( iEdg ‘ 𝐺 ) )
19 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
20 18 19 eleqtrrdi ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
21 eleq1 ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) → ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
22 21 eqcoms ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
23 20 22 syl5ibrcom ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
24 23 ralimdva ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
25 24 ex ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ UPGraph → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
26 25 com23 ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
27 26 3impia ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
28 27 impcom ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
29 lencl ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
30 ffz0hash ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
31 30 ex ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
32 oveq1 ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) )
33 nn0cn ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
34 pncan1 ( ( ♯ ‘ 𝐹 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
35 33 34 syl ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
36 32 35 sylan9eqr ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
37 36 ex ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) )
38 31 37 syld ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) )
39 29 38 syl ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) )
40 39 imp ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) )
41 40 oveq2d ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
42 41 raleqdv ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
43 42 3adant3 ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
44 43 adantl ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
45 28 44 mpbird ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
46 45 adantr ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
47 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
48 2 47 iswwlks ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
49 5 8 46 48 syl3anbrc ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ∈ ( WWalks ‘ 𝐺 ) )
50 49 ex ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )
51 50 ex ( 𝐺 ∈ UPGraph → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) )
52 4 51 sylbid ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) )
53 1 52 mpdi ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )