Metamath Proof Explorer

Theorem pthacycspth

Description: A path in an acyclic graph is a simple path. (Contributed by BTernaryTau, 21-Oct-2023)

Ref Expression
Assertion pthacycspth 
|- ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> F ( SPaths ` G ) P )

Proof

Step Hyp Ref Expression
1 cyclispth 
 |-  ( F ( Cycles ` G ) P -> F ( Paths ` G ) P )
2 1 a1i 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( Cycles ` G ) P -> F ( Paths ` G ) P ) )
3 acycgrcycl 
 |-  ( ( G e. AcyclicGraph /\ F ( Cycles ` G ) P ) -> F = (/) )
4 3 ex 
 |-  ( G e. AcyclicGraph -> ( F ( Cycles ` G ) P -> F = (/) ) )
5 4 adantr 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( Cycles ` G ) P -> F = (/) ) )
6 2 5 jcad 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( Cycles ` G ) P -> ( F ( Paths ` G ) P /\ F = (/) ) ) )
7 spthcycl 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) <-> ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) )
8 7 simplbi 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> F ( SPaths ` G ) P )
9 6 8 syl6 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( Cycles ` G ) P -> F ( SPaths ` G ) P ) )
10 pthisspthorcycl 
 |-  ( F ( Paths ` G ) P -> ( F ( SPaths ` G ) P \/ F ( Cycles ` G ) P ) )
11 10 adantl 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( SPaths ` G ) P \/ F ( Cycles ` G ) P ) )
12 orim2 
 |-  ( ( F ( Cycles ` G ) P -> F ( SPaths ` G ) P ) -> ( ( F ( SPaths ` G ) P \/ F ( Cycles ` G ) P ) -> ( F ( SPaths ` G ) P \/ F ( SPaths ` G ) P ) ) )
13 9 11 12 sylc 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> ( F ( SPaths ` G ) P \/ F ( SPaths ` G ) P ) )
14 pm1.2 
 |-  ( ( F ( SPaths ` G ) P \/ F ( SPaths ` G ) P ) -> F ( SPaths ` G ) P )
15 13 14 syl 
 |-  ( ( G e. AcyclicGraph /\ F ( Paths ` G ) P ) -> F ( SPaths ` G ) P )