Description: A pair <. F , P >. represents a path if it represents either a simple path or a cycle. The exclusivity only holds for non-trivial paths ( F =/= (/) ), see cyclnspth . (Contributed by AV, 2-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pthspthcyc | ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pthisspthorcycl | ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) | |
| 2 | spthispth | ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) | |
| 3 | cyclispth | ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) | |
| 4 | 2 3 | jaoi | ⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
| 5 | 1 4 | impbii | ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) ) |