| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cyclispth |
⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
| 2 |
1
|
a1i |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) |
| 3 |
|
acycgrcycl |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → 𝐹 = ∅ ) |
| 4 |
3
|
ex |
⊢ ( 𝐺 ∈ AcyclicGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 = ∅ ) ) |
| 5 |
4
|
adantr |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 = ∅ ) ) |
| 6 |
2 5
|
jcad |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 = ∅ ) ) ) |
| 7 |
|
spthcycl |
⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 = ∅ ) ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) |
| 8 |
7
|
simplbi |
⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 = ∅ ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) |
| 9 |
6 8
|
syl6 |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) |
| 10 |
|
pthisspthorcycl |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) |
| 11 |
10
|
adantl |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) |
| 12 |
|
orim2 |
⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) ) |
| 13 |
9 11 12
|
sylc |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) |
| 14 |
|
pm1.2 |
⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) |
| 15 |
13 14
|
syl |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) |