# Metamath Proof Explorer

## Theorem 0crct

Description: A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Assertion 0crct ${⊢}{G}\in {W}\to \left(\varnothing \mathrm{Circuits}\left({G}\right){P}↔{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 1 0trl ${⊢}{G}\in {W}\to \left(\varnothing \mathrm{Trails}\left({G}\right){P}↔{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\right)$
3 2 anbi1d ${⊢}{G}\in {W}\to \left(\left(\varnothing \mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|\varnothing \right|\right)\right)↔\left({P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\wedge {P}\left(0\right)={P}\left(\left|\varnothing \right|\right)\right)\right)$
4 iscrct ${⊢}\varnothing \mathrm{Circuits}\left({G}\right){P}↔\left(\varnothing \mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|\varnothing \right|\right)\right)$
5 hash0 ${⊢}\left|\varnothing \right|=0$
6 5 eqcomi ${⊢}0=\left|\varnothing \right|$
7 6 a1i ${⊢}{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\to 0=\left|\varnothing \right|$
8 7 fveq2d ${⊢}{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\to {P}\left(0\right)={P}\left(\left|\varnothing \right|\right)$
9 8 pm4.71i ${⊢}{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)↔\left({P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\wedge {P}\left(0\right)={P}\left(\left|\varnothing \right|\right)\right)$
10 3 4 9 3bitr4g ${⊢}{G}\in {W}\to \left(\varnothing \mathrm{Circuits}\left({G}\right){P}↔{P}:\left(0\dots 0\right)⟶\mathrm{Vtx}\left({G}\right)\right)$