Metamath Proof Explorer

Theorem pthisspthorcycl

Description: A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023)

Ref Expression
Assertion pthisspthorcycl 
|- ( F ( Paths ` G ) P -> ( F ( SPaths ` G ) P \/ F ( Cycles ` G ) P ) )

Proof

Step Hyp Ref Expression
1 pthdepisspth 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> F ( SPaths ` G ) P )
2 1 ex 
 |-  ( F ( Paths ` G ) P -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) -> F ( SPaths ` G ) P ) )
3 2 necon1bd 
 |-  ( F ( Paths ` G ) P -> ( -. F ( SPaths ` G ) P -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 3 anc2li 
 |-  ( F ( Paths ` G ) P -> ( -. F ( SPaths ` G ) P -> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
5 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
6 4 5 syl6ibr 
 |-  ( F ( Paths ` G ) P -> ( -. F ( SPaths ` G ) P -> F ( Cycles ` G ) P ) )
7 6 orrd 
 |-  ( F ( Paths ` G ) P -> ( F ( SPaths ` G ) P \/ F ( Cycles ` G ) P ) )