Metamath Proof Explorer

Theorem clwlkclwwlk

Description: A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clwlkclwwlk.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion clwlkclwwlk ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clwlkclwwlk.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 2 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) )
4 f1of1 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) → 𝐸 : dom 𝐸 –1-1→ ( Edg ‘ 𝐺 ) )
5 3 4 syl ⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1→ ( Edg ‘ 𝐺 ) )
6 clwlkclwwlklem3 ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ( Edg ‘ 𝐺 ) ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
7 5 6 syl3an1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
8 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
9 ige2m1fz ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) )
10 8 9 sylan ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) )
11 pfxlen ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑃 ) ) ) → ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
12 10 11 syldan ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
13 8 nn0cnd ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℂ )
14 1cnd ⊢ ( 𝑃 ∈ Word 𝑉 → 1 ∈ ℂ )
15 13 14 subcld ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℂ )
16 15 subid1d ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
17 16 eqcomd ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) )
18 17 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) )
19 12 18 eqtrd ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) )
20 19 oveq1d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) = ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) )
21 20 oveq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) = ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) )
22 12 oveq1d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) )
23 22 oveq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) )
24 23 eleq2d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) )
25 simpll ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → 𝑃 ∈ Word 𝑉 )
26 wrdlenge2n0 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 ≠ ∅ )
27 26 adantr ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → 𝑃 ≠ ∅ )
28 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
29 peano2zm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
30 28 29 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
31 8 30 syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
32 31 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
33 elfzom1elfzo ⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
34 32 33 sylan ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
35 pfxtrcfv ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
36 25 27 34 35 syl3anc ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
37 8 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
38 elfzom1elp1fzo ⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
39 30 38 sylan ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
40 37 39 sylan ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
41 pfxtrcfv ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
42 25 27 40 41 syl3anc ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
43 36 42 preq12d ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
44 43 eleq1d ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) ) → ( { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
45 44 ex ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 1 ) ) → ( { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ) )
46 24 45 sylbid ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) → ( { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ) )
47 46 imp ⊢ ( ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) ) → ( { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
48 21 47 raleqbidva ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) )
49 pfxtrcfvl ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) )
50 pfxtrcfv0 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) = ( 𝑃 ‘ 0 ) )
51 49 50 preq12d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } )
52 51 eleq1d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) )
53 48 52 anbi12d ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) )
54 53 bicomd ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) )
55 54 3adant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) )
56 pfxcl ⊢ ( 𝑃 ∈ Word 𝑉 → ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 )
57 56 3ad2ant2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 )
58 57 3biant1d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) )
59 55 58 bitrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) )
60 59 anbi2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) − 0 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 2 ) ) , ( 𝑃 ‘ 0 ) } ∈ ran 𝐸 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
61 7 60 bitrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
62 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
63 1 2 isclwlkupgr ⊢ ( 𝐺 ∈ UPGraph → ( 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) ) )
64 3an4anass ⊢ ( ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ↔ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
65 63 64 bitr4di ⊢ ( 𝐺 ∈ UPGraph → ( 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
66 62 65 syl ⊢ ( 𝐺 ∈ USPGraph → ( 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
67 66 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ) → ( 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
68 67 exbidv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
69 68 3adant3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ∃ 𝑓 ( ( 𝑓 ∈ Word dom 𝐸 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐸 ‘ ( 𝑓 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝑓 ) ) ) ) )
70 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
71 1 70 isclwwlk ⊢ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
72 simpl ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 ∈ Word 𝑉 )
73 nn0ge2m1nn ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ )
74 8 73 sylan ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ )
75 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
76 75 lem1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) )
77 76 a1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
78 8 77 syl ⊢ ( 𝑃 ∈ Word 𝑉 → ( 2 ≤ ( ♯ ‘ 𝑃 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
79 78 imp ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) )
80 72 74 79 3jca ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
81 80 3adant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
82 pfxn0 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ )
83 81 82 syl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ )
84 83 biantrud ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ ) ) )
85 84 bicomd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ ) ↔ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ) )
86 85 3anbi1d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
87 71 86 bitrid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
88 biid ⊢ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ↔ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 )
89 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
90 2 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
91 90 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐸
92 89 91 eqtri ⊢ ( Edg ‘ 𝐺 ) = ran 𝐸
93 92 eleq2i ⊢ ( { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
94 93 ralbii ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 )
95 92 eleq2i ⊢ ( { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 )
96 88 94 95 3anbi123i ⊢ ( ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) )
97 87 96 bitrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) )
98 97 anbi2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) − 1 ) ) { ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 𝑖 ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ∧ { ( lastS ‘ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) , ( ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ‘ 0 ) } ∈ ran 𝐸 ) ) ) )
99 61 69 98 3bitr4d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑓 𝑓 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 prefix ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∈ ( ClWWalks ‘ 𝐺 ) ) ) )