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