Metamath Proof Explorer


Definition df-cycls

Description: Define the set of all (simple) cycles (in an undirected graph).

According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory) , 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex."

According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of Bollobas p. 5.

However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017) (Revised by AV, 31-Jan-2021)

Ref Expression
Assertion df-cycls Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccycls Cycles
1 vg 𝑔
2 cvv V
3 vf 𝑓
4 vp 𝑝
5 3 cv 𝑓
6 cpths Paths
7 1 cv 𝑔
8 7 6 cfv ( Paths ‘ 𝑔 )
9 4 cv 𝑝
10 5 9 8 wbr 𝑓 ( Paths ‘ 𝑔 ) 𝑝
11 cc0 0
12 11 9 cfv ( 𝑝 ‘ 0 )
13 chash
14 5 13 cfv ( ♯ ‘ 𝑓 )
15 14 9 cfv ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) )
16 12 15 wceq ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) )
17 10 16 wa ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) )
18 17 3 4 copab { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) }
19 1 2 18 cmpt ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )
20 0 19 wceq Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )