Theorem cyclnspth

Description: A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	cyclnspth	⊢ ( 𝐹 ≠ ∅ → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		iscycl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
2		relpths	⊢ Rel ( Paths ‘ 𝐺 )
3	2	brrelex1i	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ∈ V )
4		hasheq0	⊢ ( 𝐹 ∈ V → ( ( ♯ ‘ 𝐹 ) = 0 ↔ 𝐹 = ∅ ) )
5	4	necon3bid	⊢ ( 𝐹 ∈ V → ( ( ♯ ‘ 𝐹 ) ≠ 0 ↔ 𝐹 ≠ ∅ ) )
6	5	bicomd	⊢ ( 𝐹 ∈ V → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
7	3 6	syl	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
8	7	biimpa	⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≠ 0 )
9		spthdep	⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
10	9	neneqd	⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) ≠ 0 ) → ¬ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
11	10	expcom	⊢ ( ( ♯ ‘ 𝐹 ) ≠ 0 → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ¬ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
12	8 11	syl	⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ¬ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
13	12	con2d	⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
14	13	impancom	⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ≠ ∅ → ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
15	1 14	sylbi	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ≠ ∅ → ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
16	15	com12	⊢ ( 𝐹 ≠ ∅ → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ¬ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )