Metamath Proof Explorer

Theorem 0clwlk

Description: A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 17-Feb-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0clwlk.v 
|- V = ( Vtx ` G )
Assertion 0clwlk 
|- ( G e. X -> ( (/) ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )

Proof

Step Hyp Ref Expression
1 0clwlk.v 
 |-  V = ( Vtx ` G )
2 1 0wlk 
 |-  ( G e. X -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
3 2 anbi2d 
 |-  ( G e. X -> ( ( ( P ` 0 ) = ( P ` ( # ` (/) ) ) /\ (/) ( Walks ` G ) P ) <-> ( ( P ` 0 ) = ( P ` ( # ` (/) ) ) /\ P : ( 0 ... 0 ) --> V ) ) )
4 isclwlk 
 |-  ( (/) ( ClWalks ` G ) P <-> ( (/) ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` (/) ) ) ) )
5 4 biancomi 
 |-  ( (/) ( ClWalks ` G ) P <-> ( ( P ` 0 ) = ( P ` ( # ` (/) ) ) /\ (/) ( Walks ` G ) P ) )
6 hash0 
 |-  ( # ` (/) ) = 0
7 6 eqcomi 
 |-  0 = ( # ` (/) )
8 7 fveq2i 
 |-  ( P ` 0 ) = ( P ` ( # ` (/) ) )
9 8 biantrur 
 |-  ( P : ( 0 ... 0 ) --> V <-> ( ( P ` 0 ) = ( P ` ( # ` (/) ) ) /\ P : ( 0 ... 0 ) --> V ) )
10 3 5 9 3bitr4g 
 |-  ( G e. X -> ( (/) ( ClWalks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )