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 ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )

Proof

Step Hyp Ref Expression
1 pthdepisspth ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )
2 1 ex ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
3 2 necon1bd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4 3 anc2li ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
5 iscycl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
6 4 5 imbitrrdi ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )
7 6 orrd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )