# Metamath Proof Explorer

## 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 ${⊢}\mathrm{Circuits}=\left({g}\in \mathrm{V}⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({g}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccrcts ${class}\mathrm{Circuits}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 vp ${setvar}{p}$
5 3 cv ${setvar}{f}$
6 ctrls ${class}\mathrm{Trails}$
7 1 cv ${setvar}{g}$
8 7 6 cfv ${class}\mathrm{Trails}\left({g}\right)$
9 4 cv ${setvar}{p}$
10 5 9 8 wbr ${wff}{f}\mathrm{Trails}\left({g}\right){p}$
11 cc0 ${class}0$
12 11 9 cfv ${class}{p}\left(0\right)$
13 chash ${class}\left|.\right|$
14 5 13 cfv ${class}\left|{f}\right|$
15 14 9 cfv ${class}{p}\left(\left|{f}\right|\right)$
16 12 15 wceq ${wff}{p}\left(0\right)={p}\left(\left|{f}\right|\right)$
17 10 16 wa ${wff}\left({f}\mathrm{Trails}\left({g}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)$
18 17 3 4 copab ${class}\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({g}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$
19 1 2 18 cmpt ${class}\left({g}\in \mathrm{V}⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({g}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}\right)$
20 0 19 wceq ${wff}\mathrm{Circuits}=\left({g}\in \mathrm{V}⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({g}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}\right)$