This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pthspthcyc

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 ⊢ F Paths ⁡ G P ↔ F SPaths ⁡ G P ∨ F Cycles ⁡ G P

Proof

Step Hyp Ref Expression
1 pthisspthorcycl ⊢ F Paths ⁡ G P → F SPaths ⁡ G P ∨ F Cycles ⁡ G P
2 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
3 cyclispth ⊢ F Cycles ⁡ G P → F Paths ⁡ G P
4 2 3 jaoi ⊢ F SPaths ⁡ G P ∨ F Cycles ⁡ G P → F Paths ⁡ G P
5 1 4 impbii ⊢ F Paths ⁡ G P ↔ F SPaths ⁡ G P ∨ F Cycles ⁡ G P