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

Metamath Proof Explorer

Theorem pthisspthorcycl

Description: A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023)

Ref Expression
Assertion pthisspthorcycl ⊢ F Paths ⁡ G P → F SPaths ⁡ G P ∨ F Cycles ⁡ G P

Proof

Step Hyp Ref Expression
1 pthdepisspth ⊢ F Paths ⁡ G P ∧ P ⁡ 0 ≠ P ⁡ F → F SPaths ⁡ G P
2 1 ex ⊢ F Paths ⁡ G P → P ⁡ 0 ≠ P ⁡ F → F SPaths ⁡ G P
3 2 necon1bd ⊢ F Paths ⁡ G P → ¬ F SPaths ⁡ G P → P ⁡ 0 = P ⁡ F
4 3 anc2li ⊢ F Paths ⁡ G P → ¬ F SPaths ⁡ G P → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
5 iscycl ⊢ F Cycles ⁡ G P ↔ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
6 4 5 imbitrrdi ⊢ F Paths ⁡ G P → ¬ F SPaths ⁡ G P → F Cycles ⁡ G P
7 6 orrd ⊢ F Paths ⁡ G P → F SPaths ⁡ G P ∨ F Cycles ⁡ G P