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

Metamath Proof Explorer

Theorem wlkp1lem8

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
wlkp1.l ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { 𝐶 } )
Assertion wlkp1lem8 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkp1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkp1.f ⊢ ( 𝜑 → Fun 𝐼 )
4 wlkp1.a ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 wlkp1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6 wlkp1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
7 wlkp1.d ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 wlkp1.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 wlkp1.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
10 wlkp1.e ⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 wlkp1.x ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 wlkp1.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13 wlkp1.h ⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 wlkp1.q ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 wlkp1.l ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { 𝐶 } )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem6 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
18 10 elfvexd ⊢ ( 𝜑 → 𝐺 ∈ V )
19 1 2 iswlkg ⊢ ( 𝐺 ∈ V → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
21 9 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
22 21 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 )
23 22 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
24 23 biimpi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
25 24 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
26 20 25 biimtrdi ⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
27 8 26 mpd ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
28 eqeq12 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
29 28 3adant3 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
30 simp3 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
31 simp1 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
32 31 sneqd ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → { ( 𝑄 ‘ 𝑘 ) } = { ( 𝑃 ‘ 𝑘 ) } )
33 30 32 eqeq12d ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) )
34 preq12 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
35 34 3adant3 ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
36 35 30 sseq12d ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
37 29 33 36 ifpbi123d ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
38 37 biimprd ⊢ ( ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
39 38 ral2imi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑄 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑄 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
40 17 27 39 sylc ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
41 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3 ⊢ ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )
43 5 10 7 3jca ⊢ ( 𝜑 → ( 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ ¬ 𝐵 ∈ dom 𝐼 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → ( 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ ¬ 𝐵 ∈ dom 𝐼 ) )
45 fsnunfv ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ ¬ 𝐵 ∈ dom 𝐼 ) → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) = 𝐸 )
46 44 45 syl ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) = 𝐸 )
47 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑄 ‘ 𝑥 ) = ( 𝑄 ‘ 𝑁 ) )
48 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) )
49 47 48 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) ↔ ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑥 ) )
51 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
52 lencl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
53 9 eleq1i ⊢ ( 𝑁 ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
54 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
55 53 54 sylbb1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
56 52 55 syl ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
57 8 51 56 3syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
58 57 54 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
59 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
60 58 59 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
61 49 50 60 rspcdva ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) )
62 14 fveq1i ⊢ ( 𝑄 ‘ ( 𝑁 + 1 ) ) = ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) )
63 ovex ⊢ ( 𝑁 + 1 ) ∈ V
64 1 2 3 4 5 6 7 8 9 wlkp1lem1 ⊢ ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )
65 fsnunfv ⊢ ( ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
66 63 6 64 65 mp3an2i ⊢ ( 𝜑 → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
67 62 66 eqtrid ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 + 1 ) ) = 𝐶 )
68 67 eqeq2d ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ↔ ( 𝑃 ‘ 𝑁 ) = 𝐶 ) )
69 eqcom ⊢ ( ( 𝑃 ‘ 𝑁 ) = 𝐶 ↔ 𝐶 = ( 𝑃 ‘ 𝑁 ) )
70 68 69 bitrdi ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ↔ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) )
71 sneq ⊢ ( 𝐶 = ( 𝑃 ‘ 𝑁 ) → { 𝐶 } = { ( 𝑃 ‘ 𝑁 ) } )
72 71 adantl ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → { 𝐶 } = { ( 𝑃 ‘ 𝑁 ) } )
73 16 72 eqtrd ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { ( 𝑃 ‘ 𝑁 ) } )
74 73 ex ⊢ ( 𝜑 → ( 𝐶 = ( 𝑃 ‘ 𝑁 ) → 𝐸 = { ( 𝑃 ‘ 𝑁 ) } ) )
75 70 74 sylbid ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) → 𝐸 = { ( 𝑃 ‘ 𝑁 ) } ) )
76 eqeq1 ⊢ ( ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) → ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ↔ ( 𝑃 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) )
77 sneq ⊢ ( ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) → { ( 𝑄 ‘ 𝑁 ) } = { ( 𝑃 ‘ 𝑁 ) } )
78 77 eqeq2d ⊢ ( ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) → ( 𝐸 = { ( 𝑄 ‘ 𝑁 ) } ↔ 𝐸 = { ( 𝑃 ‘ 𝑁 ) } ) )
79 76 78 imbi12d ⊢ ( ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) → ( ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) → 𝐸 = { ( 𝑄 ‘ 𝑁 ) } ) ↔ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) → 𝐸 = { ( 𝑃 ‘ 𝑁 ) } ) ) )
80 75 79 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) → ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) → 𝐸 = { ( 𝑄 ‘ 𝑁 ) } ) ) )
81 61 80 mpd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) → 𝐸 = { ( 𝑄 ‘ 𝑁 ) } ) )
82 81 imp ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → 𝐸 = { ( 𝑄 ‘ 𝑁 ) } )
83 42 46 82 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } )
84 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem7 ⊢ ( 𝜑 → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) ) → { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )
86 83 85 ifpimpda ⊢ ( 𝜑 → if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) )
87 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )
88 87 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
89 fzosplitsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
90 57 89 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
91 88 90 eqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
92 91 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
93 ralunb ⊢ ( ∀ 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ { 𝑁 } if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
94 93 a1i ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ { 𝑁 } if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) ) )
95 9 fvexi ⊢ 𝑁 ∈ V
96 wkslem1 ⊢ ( 𝑘 = 𝑁 → ( if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) ) )
97 96 ralsng ⊢ ( 𝑁 ∈ V → ( ∀ 𝑘 ∈ { 𝑁 } if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) ) )
98 95 97 mp1i ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 𝑁 } if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) ) )
99 98 anbi2d ⊢ ( 𝜑 → ( ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ { 𝑁 } if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) ↔ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ∧ if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) ) ) )
100 92 94 99 3bitrd ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ∧ if- ( ( 𝑄 ‘ 𝑁 ) = ( 𝑄 ‘ ( 𝑁 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = { ( 𝑄 ‘ 𝑁 ) } , { ( 𝑄 ‘ 𝑁 ) , ( 𝑄 ‘ ( 𝑁 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ) ) ) )
101 40 86 100 mpbir2and ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) = { ( 𝑄 ‘ 𝑘 ) } , { ( 𝑄 ‘ 𝑘 ) , ( 𝑄 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )