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

Metamath Proof Explorer

Theorem wlk1walk

Description: A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypothesis wlk1walk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wlk1walk ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wlk1walk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 3 4 iswlk ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ) )
6 fvex ⊢ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∈ V
7 6 inex1 ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V
8 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
9 8 sseli ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
10 wkslem1 ⊢ ( 𝑖 = 𝑘 → ( if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
11 10 rspcv ⊢ ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) → if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
12 9 11 syl ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) → if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
13 12 imp ⊢ ( ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
14 elfzofz ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) )
15 fz1fzo0m1 ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 wkslem1 ⊢ ( 𝑖 = ( 𝑘 − 1 ) → ( if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
17 16 rspcv ⊢ ( ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) → if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
18 14 15 17 3syl ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) → if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
19 18 imp ⊢ ( ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) )
20 df-ifp ⊢ ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
21 elfzoelz ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑘 ∈ ℤ )
22 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
23 eqidd ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 − 1 ) = ( 𝑘 − 1 ) )
24 npcan1 ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
25 wkslem2 ⊢ ( ( ( 𝑘 − 1 ) = ( 𝑘 − 1 ) ∧ ( ( 𝑘 − 1 ) + 1 ) = 𝑘 ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ↔ if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
26 23 24 25 syl2anc ⊢ ( 𝑘 ∈ ℂ → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ↔ if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
27 21 22 26 3syl ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ↔ if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
28 df-ifp ⊢ ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ↔ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) ∨ ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) )
29 sneq ⊢ ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) → { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) } )
30 29 eqeq2d ⊢ ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } ) )
31 fvex ⊢ ( 𝑃 ‘ 𝑘 ) ∈ V
32 31 snid ⊢ ( 𝑃 ‘ 𝑘 ) ∈ { ( 𝑃 ‘ 𝑘 ) }
33 1 fveq1i ⊢ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) )
34 33 eleq2i ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
35 eleq2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ { ( 𝑃 ‘ 𝑘 ) } ) )
36 34 35 bitrid ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ { ( 𝑃 ‘ 𝑘 ) } ) )
37 32 36 mpbiri ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
38 eleq2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ { ( 𝑃 ‘ 𝑘 ) } ) )
39 32 38 mpbiri ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
40 1 fveq1i ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) )
41 39 40 eleqtrrdi ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
42 37 41 anim12i ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
43 42 ex ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
44 30 43 biimtrdi ⊢ ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
45 44 imp ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
46 45 com12 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
47 46 adantl ⊢ ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) → ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
48 fvex ⊢ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V
49 31 48 prss ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
50 1 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
51 50 fveq1i ⊢ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) )
52 51 eleq2i ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
53 52 biimpi ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
54 53 adantr ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
55 49 54 sylbir ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
56 37 55 anim12i ⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
57 56 ex ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
58 30 57 biimtrdi ⊢ ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
59 58 imp ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
60 59 com12 ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
61 60 adantl ⊢ ( ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
62 47 61 jaoi ⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
63 62 com12 ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) → ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
64 fvex ⊢ ( 𝑃 ‘ ( 𝑘 − 1 ) ) ∈ V
65 64 31 prss ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ↔ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
66 50 fveq1i ⊢ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) )
67 66 eleq2i ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
68 67 biimpi ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
69 40 eleq2i ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
70 69 38 bitrid ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∈ { ( 𝑃 ‘ 𝑘 ) } ) )
71 32 70 mpbiri ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
72 68 71 anim12i ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
73 72 ex ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
74 73 adantl ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
75 65 74 sylbir ⊢ ( { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
76 75 adantl ⊢ ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
77 76 com12 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
78 77 adantl ⊢ ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
79 67 52 anbi12i ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
80 79 biimpi ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
81 80 ex ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
82 81 adantl ⊢ ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
83 65 82 sylbir ⊢ ( { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
84 83 adantl ⊢ ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
85 84 com12 ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
86 85 adantr ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
87 49 86 sylbir ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
88 87 adantl ⊢ ( ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
89 78 88 jaoi ⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
90 89 com12 ⊢ ( ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
91 63 90 jaoi ⊢ ( ( ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } ) ∨ ( ¬ ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) ∧ { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
92 28 91 sylbi ⊢ ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ 𝑘 ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ 𝑘 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
93 27 92 biimtrdi ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
94 93 com3r ⊢ ( ( ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) ∨ ( ¬ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
95 20 94 sylbi ⊢ ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
96 95 com12 ⊢ ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
97 96 adantr ⊢ ( ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( if- ( ( 𝑃 ‘ ( 𝑘 − 1 ) ) = ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) = { ( 𝑃 ‘ ( 𝑘 − 1 ) ) } , { ( 𝑃 ‘ ( 𝑘 − 1 ) ) , ( 𝑃 ‘ ( ( 𝑘 − 1 ) + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
98 13 19 97 mp2d ⊢ ( ( 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
99 98 ancoms ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
100 inelcm ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≠ ∅ )
101 99 100 syl ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≠ ∅ )
102 hashge1 ⊢ ( ( ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ V ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≠ ∅ ) → 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
103 7 101 102 sylancr ⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
104 103 ralrimiva ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
105 104 3ad2ant3 ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
106 5 105 biimtrdi ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
107 2 106 mpcom ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 1 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )