df-crcts

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 = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land p (0) = p (\|f\|))\})$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-crcts

Detailed syntax breakdown