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 ⊢ F ≠ ∅ → F Cycles ⁡ G P → ¬ F SPaths ⁡ G P

Proof

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