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 e. W -> ( (/) ( Circuits ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
2	1	0trl	|- ( G e. W -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )
3	2	anbi1d	|- ( G e. W -> ( ( (/) ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) <-> ( P : ( 0 ... 0 ) --> ( Vtx ` G ) /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) ) )
4		iscrct	|- ( (/) ( Circuits ` G ) P <-> ( (/) ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) )
5		hash0	|- ( # ` (/) ) = 0
6	5	eqcomi	|- 0 = ( # ` (/) )
7	6	a1i	|- ( P : ( 0 ... 0 ) --> ( Vtx ` G ) -> 0 = ( # ` (/) ) )
8	7	fveq2d	|- ( P : ( 0 ... 0 ) --> ( Vtx ` G ) -> ( P ` 0 ) = ( P ` ( # ` (/) ) ) )
9	8	pm4.71i	|- ( P : ( 0 ... 0 ) --> ( Vtx ` G ) <-> ( P : ( 0 ... 0 ) --> ( Vtx ` G ) /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) )
10	3 4 9	3bitr4g	|- ( G e. W -> ( (/) ( Circuits ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )