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	syl6ibr	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )
7	6	orrd	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∨ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )