# Metamath Proof Explorer

## Theorem cycliscrct

Description: A cycle is a circuit. (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 cycliscrct ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to {F}\mathrm{Circuits}\left({G}\right){P}$

### Proof

Step Hyp Ref Expression
1 pthistrl ${⊢}{F}\mathrm{Paths}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
2 1 anim1i ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
3 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)$
4 iscrct ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
5 2 3 4 3imtr4i ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to {F}\mathrm{Circuits}\left({G}\right){P}$