This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkres

Description: The restriction <. H , Q >. of a walk <. F , P >. to an initial segment of the walk (of length N ) forms a walk on the subgraph S consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 5-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses wlkres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkres.d ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
wlkres.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
wlkres.e ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
wlkres.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
wlkres.q ⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
Assertion wlkres ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )

Proof

Step Hyp Ref Expression
1 wlkres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkres.d ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 wlkres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 wlkres.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
6 wlkres.e ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
7 wlkres.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
8 wlkres.q ⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
9 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
10 pfxwrdsymb ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝐹 prefix 𝑁 ) ∈ Word ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
11 3 9 10 3syl ⊢ ( 𝜑 → ( 𝐹 prefix 𝑁 ) ∈ Word ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
12 7 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝐹 prefix 𝑁 ) )
13 6 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
14 3 9 syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
15 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
16 fimass ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 )
17 14 15 16 3syl ⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 )
18 ssdmres ⊢ ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 ↔ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
19 17 18 sylib ⊢ ( 𝜑 → dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
20 13 19 eqtrd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
21 wrdeq ⊢ ( dom ( iEdg ‘ 𝑆 ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) → Word dom ( iEdg ‘ 𝑆 ) = Word ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
22 20 21 syl ⊢ ( 𝜑 → Word dom ( iEdg ‘ 𝑆 ) = Word ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
23 11 12 22 3eltr4d ⊢ ( 𝜑 → 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) )
24 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
25 3 24 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
26 5 feq3d ⊢ ( 𝜑 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝑆 ) ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
27 25 26 mpbird ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝑆 ) )
28 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
29 28 4 sselid ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
30 elfzuz3 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
31 fzss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
32 29 30 31 3syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
33 27 32 fssresd ⊢ ( 𝜑 → ( 𝑃 ↾ ( 0 ... 𝑁 ) ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝑆 ) )
34 7 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 prefix 𝑁 ) )
35 pfxlen ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝑁 ) ) = 𝑁 )
36 14 29 35 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 prefix 𝑁 ) ) = 𝑁 )
37 34 36 eqtrid ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )
38 37 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐻 ) ) = ( 0 ... 𝑁 ) )
39 38 feq2d ⊢ ( 𝜑 → ( ( 𝑃 ↾ ( 0 ... 𝑁 ) ) : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ↔ ( 𝑃 ↾ ( 0 ... 𝑁 ) ) : ( 0 ... 𝑁 ) ⟶ ( Vtx ‘ 𝑆 ) ) )
40 33 39 mpbird ⊢ ( 𝜑 → ( 𝑃 ↾ ( 0 ... 𝑁 ) ) : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) )
41 8 feq1i ⊢ ( 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ↔ ( 𝑃 ↾ ( 0 ... 𝑁 ) ) : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) )
42 40 41 sylibr ⊢ ( 𝜑 → 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) )
43 1 2 wlkprop ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
44 3 43 syl ⊢ ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
46 37 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ 𝑁 ) )
47 46 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ↔ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) )
48 8 fveq1i ⊢ ( 𝑄 ‘ 𝑥 ) = ( ( 𝑃 ↾ ( 0 ... 𝑁 ) ) ‘ 𝑥 )
49 fzossfz ⊢ ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
50 49 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
51 50 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ( 0 ... 𝑁 ) )
52 51 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝑁 ) ) ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) )
53 48 52 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) )
54 8 fveq1i ⊢ ( 𝑄 ‘ ( 𝑥 + 1 ) ) = ( ( 𝑃 ↾ ( 0 ... 𝑁 ) ) ‘ ( 𝑥 + 1 ) )
55 fzofzp1 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝑁 ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝑁 ) )
57 56 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝑁 ) ) ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) )
58 54 57 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) )
59 53 58 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) )
60 59 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ) )
61 47 60 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ) )
62 61 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) )
63 14 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) )
64 15 ffund ⊢ ( 𝐹 ∈ Word dom 𝐼 → Fun 𝐹 )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) → Fun 𝐹 )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → Fun 𝐹 )
67 fdm ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
68 elfzouz2 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
69 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
70 4 68 69 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
71 sseq2 ⊢ ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ 𝑁 ) ⊆ dom 𝐹 ↔ ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
72 70 71 imbitrrid ⊢ ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ dom 𝐹 ) )
73 15 67 72 3syl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ dom 𝐹 ) )
74 73 impcom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) → ( 0 ..^ 𝑁 ) ⊆ dom 𝐹 )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ 𝑁 ) ⊆ dom 𝐹 )
76 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
77 66 75 76 resfvresima ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ Word dom 𝐼 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
78 63 77 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
79 78 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) )
80 79 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) ) )
81 47 80 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) ) )
82 81 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) )
83 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
84 7 fveq1i ⊢ ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 prefix 𝑁 ) ‘ 𝑥 )
85 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → 𝐹 ∈ Word dom 𝐼 )
86 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
87 pfxres ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝑁 ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
88 85 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐹 prefix 𝑁 ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
89 88 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( 𝐹 prefix 𝑁 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) )
90 84 89 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) )
91 83 90 fveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ) )
92 82 91 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) )
93 62 92 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
94 4 68 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
95 37 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( ♯ ‘ 𝐻 ) ) = ( ℤ≥ ‘ 𝑁 ) )
96 94 95 eleqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐻 ) ) )
97 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐻 ) ) → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
98 96 97 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
99 98 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
100 wkslem1 ⊢ ( 𝑘 = 𝑥 → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
101 100 rspcv ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
102 99 101 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
103 eqeq12 ⊢ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) ↔ ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) )
104 103 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) ↔ ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) )
105 simpr ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) )
106 sneq ⊢ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) → { ( 𝑃 ‘ 𝑥 ) } = { ( 𝑄 ‘ 𝑥 ) } )
107 106 adantr ⊢ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) → { ( 𝑃 ‘ 𝑥 ) } = { ( 𝑄 ‘ 𝑥 ) } )
108 107 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → { ( 𝑃 ‘ 𝑥 ) } = { ( 𝑄 ‘ 𝑥 ) } )
109 105 108 eqeq12d ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } ↔ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } ) )
110 preq12 ⊢ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } )
111 110 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } )
112 111 105 sseq12d ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
113 104 109 112 ifpbi123d ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
114 113 biimpd ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑥 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) } , { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
115 93 102 114 sylsyld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
116 115 com12 ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
117 116 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) )
118 45 117 mpcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) → if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
119 118 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
120 1 2 3 4 5 wlkreslem ⊢ ( 𝜑 → 𝑆 ∈ V )
121 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
122 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
123 121 122 iswlkg ⊢ ( 𝑆 ∈ V → ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
124 120 123 syl ⊢ ( 𝜑 → ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ∈ Word dom ( iEdg ‘ 𝑆 ) ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ ( 𝑥 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) = { ( 𝑄 ‘ 𝑥 ) } , { ( 𝑄 ‘ 𝑥 ) , ( 𝑄 ‘ ( 𝑥 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑥 ) ) ) ) ) )
125 23 42 119 124 mpbir3and ⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )