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\leftrightarrow 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\leftrightarrow 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)\leftrightarrow \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\leftrightarrow \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)\leftrightarrow \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\leftrightarrow P:\left(0\dots 0\right)⟶\mathrm{Vtx}\left(G\right)\right)$$