# Metamath Proof Explorer

## Theorem crcts

Description: The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021)

Ref Expression
Assertion crcts ${⊢}\mathrm{Circuits}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 biidd ${⊢}\left(\top \wedge {g}={G}\right)\to \left({p}\left(0\right)={p}\left(\left|{f}\right|\right)↔{p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)$
2 wksv ${⊢}\left\{⟨{f},{p}⟩|{f}\mathrm{Walks}\left({G}\right){p}\right\}\in \mathrm{V}$
3 trliswlk ${⊢}{f}\mathrm{Trails}\left({G}\right){p}\to {f}\mathrm{Walks}\left({G}\right){p}$
4 3 ssopab2i ${⊢}\left\{⟨{f},{p}⟩|{f}\mathrm{Trails}\left({G}\right){p}\right\}\subseteq \left\{⟨{f},{p}⟩|{f}\mathrm{Walks}\left({G}\right){p}\right\}$
5 2 4 ssexi ${⊢}\left\{⟨{f},{p}⟩|{f}\mathrm{Trails}\left({G}\right){p}\right\}\in \mathrm{V}$
6 5 a1i ${⊢}\top \to \left\{⟨{f},{p}⟩|{f}\mathrm{Trails}\left({G}\right){p}\right\}\in \mathrm{V}$
7 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)$
8 1 6 7 fvmptopab ${⊢}\top \to \mathrm{Circuits}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$
9 8 mptru ${⊢}\mathrm{Circuits}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$