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 
|- I = ( iEdg ` G )
Assertion wlk1walk 
|- ( F ( Walks ` G ) P -> A. k e. ( 1 ..^ ( # ` F ) ) 1 <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) )

Proof

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