# 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}\ne \varnothing \to \left({F}\mathrm{Cycles}\left({G}\right){P}\to ¬{F}\mathrm{SPaths}\left({G}\right){P}\right)$

### Proof

Step Hyp Ref Expression
1 iscycl ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}↔\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
2 relpths ${⊢}\mathrm{Rel}\mathrm{Paths}\left({G}\right)$
3 2 brrelex1i ${⊢}{F}\mathrm{Paths}\left({G}\right){P}\to {F}\in \mathrm{V}$
4 hasheq0 ${⊢}{F}\in \mathrm{V}\to \left(\left|{F}\right|=0↔{F}=\varnothing \right)$
5 4 necon3bid ${⊢}{F}\in \mathrm{V}\to \left(\left|{F}\right|\ne 0↔{F}\ne \varnothing \right)$
6 5 bicomd ${⊢}{F}\in \mathrm{V}\to \left({F}\ne \varnothing ↔\left|{F}\right|\ne 0\right)$
7 3 6 syl ${⊢}{F}\mathrm{Paths}\left({G}\right){P}\to \left({F}\ne \varnothing ↔\left|{F}\right|\ne 0\right)$
8 7 biimpa ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {F}\ne \varnothing \right)\to \left|{F}\right|\ne 0$
9 spthdep ${⊢}\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge \left|{F}\right|\ne 0\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)$
10 9 neneqd ${⊢}\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge \left|{F}\right|\ne 0\right)\to ¬{P}\left(0\right)={P}\left(\left|{F}\right|\right)$
11 10 expcom ${⊢}\left|{F}\right|\ne 0\to \left({F}\mathrm{SPaths}\left({G}\right){P}\to ¬{P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
12 8 11 syl ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {F}\ne \varnothing \right)\to \left({F}\mathrm{SPaths}\left({G}\right){P}\to ¬{P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
13 12 con2d ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {F}\ne \varnothing \right)\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to ¬{F}\mathrm{SPaths}\left({G}\right){P}\right)$
14 13 impancom ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left({F}\ne \varnothing \to ¬{F}\mathrm{SPaths}\left({G}\right){P}\right)$
15 1 14 sylbi ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to \left({F}\ne \varnothing \to ¬{F}\mathrm{SPaths}\left({G}\right){P}\right)$
16 15 com12 ${⊢}{F}\ne \varnothing \to \left({F}\mathrm{Cycles}\left({G}\right){P}\to ¬{F}\mathrm{SPaths}\left({G}\right){P}\right)$