This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscycl

Description: Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Assertion iscycl 
|- ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 cycls 
 |-  ( Cycles ` G ) = { <. f , p >. | ( f ( Paths ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) }
2 fveq1 
 |-  ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
3 2 adantl 
 |-  ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) )
4 simpr 
 |-  ( ( f = F /\ p = P ) -> p = P )
5 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
6 5 adantr 
 |-  ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) )
7 4 6 fveq12d 
 |-  ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) )
8 3 7 eqeq12d 
 |-  ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = ( p ` ( # ` f ) ) <-> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
9 relpths 
 |-  Rel ( Paths ` G )
10 1 8 9 brfvopabrbr 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )