Definition df-crcts

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

According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory) , 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...".

Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of Bollobas p. 5.), a circuit is a closed trail without repeated edges. So the circuit is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... 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-crcts	⊢ Circuits = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrcts	⊢ Circuits
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		vp	⊢ 𝑝
5	3	cv	⊢ 𝑓
6		ctrls	⊢ Trails
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Trails ‘ 𝑔 )
9	4	cv	⊢ 𝑝
10	5 9 8	wbr	⊢ 𝑓 ( Trails ‘ 𝑔 ) 𝑝
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	⊢ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) )
18	17 3 4	copab	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) }
19	1 2 18	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )
20	0 19	wceq	⊢ Circuits = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )