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 ⊢ G ∈ USHGraph → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P

Proof

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