Metamath Proof Explorer


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 ‘ 𝐺 ) 𝑃 ) )