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

Metamath Proof Explorer

Theorem cyclnumvtx

Description: The number of vertices of a (non-trivial) cycle is the number of edges in the cycle. (Contributed by AV, 5-Oct-2025)

Ref Expression
Assertion cyclnumvtx 
|- ( ( 1 <_ ( # ` F ) /\ F ( Cycles ` G ) P ) -> ( # ` ran P ) = ( # ` F ) )

Proof

Step Hyp Ref Expression
1 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
2 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
5 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
6 elnnnn0c 
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) )
7 frel 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> Rel P )
8 7 3ad2ant1 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> Rel P )
9 fz1ssfz0 
 |-  ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
10 fdm 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> dom P = ( 0 ... ( # ` F ) ) )
11 9 10 sseqtrrid 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( 1 ... ( # ` F ) ) C_ dom P )
12 11 3ad2ant1 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( 1 ... ( # ` F ) ) C_ dom P )
13 8 12 jca 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) )
14 10 3ad2ant1 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> dom P = ( 0 ... ( # ` F ) ) )
15 14 difeq1d 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( dom P \ ( 1 ... ( # ` F ) ) ) = ( ( 0 ... ( # ` F ) ) \ ( 1 ... ( # ` F ) ) ) )
16 nnnn0 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. NN0 )
17 fz0sn0fz1 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ... ( # ` F ) ) = ( { 0 } u. ( 1 ... ( # ` F ) ) ) )
18 16 17 syl 
 |-  ( ( # ` F ) e. NN -> ( 0 ... ( # ` F ) ) = ( { 0 } u. ( 1 ... ( # ` F ) ) ) )
19 18 difeq1d 
 |-  ( ( # ` F ) e. NN -> ( ( 0 ... ( # ` F ) ) \ ( 1 ... ( # ` F ) ) ) = ( ( { 0 } u. ( 1 ... ( # ` F ) ) ) \ ( 1 ... ( # ` F ) ) ) )
20 1e0p1 
 |-  1 = ( 0 + 1 )
21 20 oveq1i 
 |-  ( 1 ... ( # ` F ) ) = ( ( 0 + 1 ) ... ( # ` F ) )
22 21 ineq2i 
 |-  ( { 0 } i^i ( 1 ... ( # ` F ) ) ) = ( { 0 } i^i ( ( 0 + 1 ) ... ( # ` F ) ) )
23 22 a1i 
 |-  ( ( # ` F ) e. NN -> ( { 0 } i^i ( 1 ... ( # ` F ) ) ) = ( { 0 } i^i ( ( 0 + 1 ) ... ( # ` F ) ) ) )
24 elnn0uz 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( ZZ>= ` 0 ) )
25 16 24 sylib 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. ( ZZ>= ` 0 ) )
26 fzpreddisj 
 |-  ( ( # ` F ) e. ( ZZ>= ` 0 ) -> ( { 0 } i^i ( ( 0 + 1 ) ... ( # ` F ) ) ) = (/) )
27 25 26 syl 
 |-  ( ( # ` F ) e. NN -> ( { 0 } i^i ( ( 0 + 1 ) ... ( # ` F ) ) ) = (/) )
28 23 27 eqtrd 
 |-  ( ( # ` F ) e. NN -> ( { 0 } i^i ( 1 ... ( # ` F ) ) ) = (/) )
29 undif5 
 |-  ( ( { 0 } i^i ( 1 ... ( # ` F ) ) ) = (/) -> ( ( { 0 } u. ( 1 ... ( # ` F ) ) ) \ ( 1 ... ( # ` F ) ) ) = { 0 } )
30 28 29 syl 
 |-  ( ( # ` F ) e. NN -> ( ( { 0 } u. ( 1 ... ( # ` F ) ) ) \ ( 1 ... ( # ` F ) ) ) = { 0 } )
31 19 30 eqtrd 
 |-  ( ( # ` F ) e. NN -> ( ( 0 ... ( # ` F ) ) \ ( 1 ... ( # ` F ) ) ) = { 0 } )
32 31 3ad2ant2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( 0 ... ( # ` F ) ) \ ( 1 ... ( # ` F ) ) ) = { 0 } )
33 15 32 eqtrd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( dom P \ ( 1 ... ( # ` F ) ) ) = { 0 } )
34 33 imaeq2d 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) = ( P " { 0 } ) )
35 ffn 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P Fn ( 0 ... ( # ` F ) ) )
36 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
37 16 36 syl 
 |-  ( ( # ` F ) e. NN -> 0 e. ( 0 ... ( # ` F ) ) )
38 35 37 anim12i 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN ) -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
39 38 3adant3 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
40 fnsnfv 
 |-  ( ( P Fn ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) -> { ( P ` 0 ) } = ( P " { 0 } ) )
41 39 40 syl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> { ( P ` 0 ) } = ( P " { 0 } ) )
42 34 41 eqtr4d 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) = { ( P ` 0 ) } )
43 elfz1end 
 |-  ( ( # ` F ) e. NN <-> ( # ` F ) e. ( 1 ... ( # ` F ) ) )
44 43 biimpi 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. ( 1 ... ( # ` F ) ) )
45 44 3ad2ant2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( # ` F ) e. ( 1 ... ( # ` F ) ) )
46 45 fvresd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( P |` ( 1 ... ( # ` F ) ) ) ` ( # ` F ) ) = ( P ` ( # ` F ) ) )
47 ffun 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> Fun P )
48 47 funresd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> Fun ( P |` ( 1 ... ( # ` F ) ) ) )
49 48 3ad2ant1 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> Fun ( P |` ( 1 ... ( # ` F ) ) ) )
50 ssdmres 
 |-  ( ( 1 ... ( # ` F ) ) C_ dom P <-> dom ( P |` ( 1 ... ( # ` F ) ) ) = ( 1 ... ( # ` F ) ) )
51 12 50 sylib 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> dom ( P |` ( 1 ... ( # ` F ) ) ) = ( 1 ... ( # ` F ) ) )
52 45 51 eleqtrrd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( # ` F ) e. dom ( P |` ( 1 ... ( # ` F ) ) ) )
53 49 52 jca 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( Fun ( P |` ( 1 ... ( # ` F ) ) ) /\ ( # ` F ) e. dom ( P |` ( 1 ... ( # ` F ) ) ) ) )
54 fvelrn 
 |-  ( ( Fun ( P |` ( 1 ... ( # ` F ) ) ) /\ ( # ` F ) e. dom ( P |` ( 1 ... ( # ` F ) ) ) ) -> ( ( P |` ( 1 ... ( # ` F ) ) ) ` ( # ` F ) ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) )
55 53 54 syl 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( P |` ( 1 ... ( # ` F ) ) ) ` ( # ` F ) ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) )
56 46 55 eqeltrrd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` ( # ` F ) ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) )
57 eleq1 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( P ` 0 ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
58 57 3ad2ant3 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( P ` 0 ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) <-> ( P ` ( # ` F ) ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
59 56 58 mpbird 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` 0 ) e. ran ( P |` ( 1 ... ( # ` F ) ) ) )
60 59 snssd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> { ( P ` 0 ) } C_ ran ( P |` ( 1 ... ( # ` F ) ) ) )
61 42 60 eqsstrd 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) )
62 13 61 jca 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ ( # ` F ) e. NN /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
63 62 3exp 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) e. NN -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) )
64 63 com3l 
 |-  ( ( # ` F ) e. NN -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) )
65 6 64 sylbir 
 |-  ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) )
66 65 expcom 
 |-  ( 1 <_ ( # ` F ) -> ( ( # ` F ) e. NN0 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) ) )
67 66 com14 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` F ) e. NN0 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( 1 <_ ( # ` F ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) ) )
68 4 5 67 sylc 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( 1 <_ ( # ` F ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) )
69 2 68 syl 
 |-  ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( 1 <_ ( # ` F ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) ) )
70 69 imp 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( 1 <_ ( # ` F ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) )
71 1 70 sylbi 
 |-  ( F ( Cycles ` G ) P -> ( 1 <_ ( # ` F ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) ) )
72 71 impcom 
 |-  ( ( 1 <_ ( # ` F ) /\ F ( Cycles ` G ) P ) -> ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
73 imadifssran 
 |-  ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) -> ( ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) -> ran P = ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
74 73 imp 
 |-  ( ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) -> ran P = ran ( P |` ( 1 ... ( # ` F ) ) ) )
75 74 fveq2d 
 |-  ( ( ( Rel P /\ ( 1 ... ( # ` F ) ) C_ dom P ) /\ ( P " ( dom P \ ( 1 ... ( # ` F ) ) ) ) C_ ran ( P |` ( 1 ... ( # ` F ) ) ) ) -> ( # ` ran P ) = ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
76 72 75 syl 
 |-  ( ( 1 <_ ( # ` F ) /\ F ( Cycles ` G ) P ) -> ( # ` ran P ) = ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
77 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
78 pthdifv 
 |-  ( F ( Paths ` G ) P -> ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )
79 47 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> Fun P )
80 fzfid 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ... ( # ` F ) ) e. Fin )
81 fnfi 
 |-  ( ( P Fn ( 0 ... ( # ` F ) ) /\ ( 0 ... ( # ` F ) ) e. Fin ) -> P e. Fin )
82 35 80 81 syl2anr 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> P e. Fin )
83 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
84 83 a1i 
 |-  ( ( # ` F ) e. NN0 -> 1 e. ( ZZ>= ` 0 ) )
85 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
86 84 85 syl 
 |-  ( ( # ` F ) e. NN0 -> ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
87 86 adantr 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
88 10 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> dom P = ( 0 ... ( # ` F ) ) )
89 87 88 sseqtrrd 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( 1 ... ( # ` F ) ) C_ dom P )
90 79 82 89 3jca 
 |-  ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) )
91 90 ex 
 |-  ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) ) )
92 5 4 91 sylc 
 |-  ( F ( Walks ` G ) P -> ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) )
93 2 92 syl 
 |-  ( F ( Paths ` G ) P -> ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) )
94 93 adantr 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) )
95 hashres 
 |-  ( ( Fun P /\ P e. Fin /\ ( 1 ... ( # ` F ) ) C_ dom P ) -> ( # ` ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` ( 1 ... ( # ` F ) ) ) )
96 94 95 syl 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( # ` ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` ( 1 ... ( # ` F ) ) ) )
97 ovexd 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( 1 ... ( # ` F ) ) e. _V )
98 hashf1rn 
 |-  ( ( ( 1 ... ( # ` F ) ) e. _V /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( # ` ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
99 97 98 sylancom 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( # ` ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) )
100 2 5 syl 
 |-  ( F ( Paths ` G ) P -> ( # ` F ) e. NN0 )
101 hashfz1 
 |-  ( ( # ` F ) e. NN0 -> ( # ` ( 1 ... ( # ` F ) ) ) = ( # ` F ) )
102 100 101 syl 
 |-  ( F ( Paths ` G ) P -> ( # ` ( 1 ... ( # ` F ) ) ) = ( # ` F ) )
103 102 adantr 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( # ` ( 1 ... ( # ` F ) ) ) = ( # ` F ) )
104 96 99 103 3eqtr3d 
 |-  ( ( F ( Paths ` G ) P /\ ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) -> ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` F ) )
105 104 ex 
 |-  ( F ( Paths ` G ) P -> ( ( P |` ( 1 ... ( # ` F ) ) ) : ( 1 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` F ) ) )
106 78 105 mpd 
 |-  ( F ( Paths ` G ) P -> ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` F ) )
107 77 106 syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` F ) )
108 107 adantl 
 |-  ( ( 1 <_ ( # ` F ) /\ F ( Cycles ` G ) P ) -> ( # ` ran ( P |` ( 1 ... ( # ` F ) ) ) ) = ( # ` F ) )
109 76 108 eqtrd 
 |-  ( ( 1 <_ ( # ` F ) /\ F ( Cycles ` G ) P ) -> ( # ` ran P ) = ( # ` F ) )