Metamath Proof Explorer

Theorem 0cycl

Description: A pair of an empty set (of edges) and a second set (of vertices) is a cycle 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 0cycl 
|- ( G e. W -> ( (/) ( Cycles ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 0pth 
 |-  ( G e. W -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )
3 2 anbi1d 
 |-  ( G e. W -> ( ( (/) ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) <-> ( P : ( 0 ... 0 ) --> ( Vtx ` G ) /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) ) )
4 iscycl 
 |-  ( (/) ( Cycles ` G ) P <-> ( (/) ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) )
5 hash0 
 |-  ( # ` (/) ) = 0
6 5 eqcomi 
 |-  0 = ( # ` (/) )
7 6 fveq2i 
 |-  ( P ` 0 ) = ( P ` ( # ` (/) ) )
8 7 biantru 
 |-  ( P : ( 0 ... 0 ) --> ( Vtx ` G ) <-> ( P : ( 0 ... 0 ) --> ( Vtx ` G ) /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) )
9 3 4 8 3bitr4g 
 |-  ( G e. W -> ( (/) ( Cycles ` G ) P <-> P : ( 0 ... 0 ) --> ( Vtx ` G ) ) )