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

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