Metamath Proof Explorer

Theorem cyclispthon

Description: A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion cyclispthon 
|- ( F ( Cycles ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` 0 ) ) P )

Proof

Step Hyp Ref Expression
1 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
2 pthonpth 
 |-  ( F ( Paths ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P )
3 1 2 syl 
 |-  ( F ( Cycles ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P )
4 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
5 4 simprbi 
 |-  ( F ( Cycles ` G ) P -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
6 5 oveq2d 
 |-  ( F ( Cycles ` G ) P -> ( ( P ` 0 ) ( PathsOn ` G ) ( P ` 0 ) ) = ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) )
7 6 breqd 
 |-  ( F ( Cycles ` G ) P -> ( F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` 0 ) ) P <-> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` ( # ` F ) ) ) P ) )
8 3 7 mpbird 
 |-  ( F ( Cycles ` G ) P -> F ( ( P ` 0 ) ( PathsOn ` G ) ( P ` 0 ) ) P )