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 ∈ 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 ∈ AcyclicGraph ∧ F Paths ⁡ G P → F Cycles ⁡ G P → F Paths ⁡ G P
3 acycgrcycl ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → F = ∅
4 3 ex ⊢ G ∈ AcyclicGraph → F Cycles ⁡ G P → F = ∅
5 4 adantr ⊢ G ∈ AcyclicGraph ∧ F Paths ⁡ G P → F Cycles ⁡ G P → F = ∅
6 2 5 jcad ⊢ G ∈ 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 ∈ 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 ∈ 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 ∈ 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 ∈ AcyclicGraph ∧ F Paths ⁡ G P → F SPaths ⁡ G P