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