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 ≤ ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ ran 𝑃 ) = ( ♯ ‘ 𝐹 ) )

Proof

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