# Metamath Proof Explorer

## Theorem iscycl

Description: Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 cycls ${⊢}\mathrm{Cycles}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Paths}\left({G}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$
2 fveq1 ${⊢}{p}={P}\to {p}\left(0\right)={P}\left(0\right)$
3 2 adantl ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(0\right)={P}\left(0\right)$
4 simpr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}={P}$
5 fveq2 ${⊢}{f}={F}\to \left|{f}\right|=\left|{F}\right|$
6 5 adantr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left|{f}\right|=\left|{F}\right|$
7 4 6 fveq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(\left|{f}\right|\right)={P}\left(\left|{F}\right|\right)$
8 3 7 eqeq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({p}\left(0\right)={p}\left(\left|{f}\right|\right)↔{P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
9 relpths ${⊢}\mathrm{Rel}\mathrm{Paths}\left({G}\right)$
10 1 8 9 brfvopabrbr ${⊢}{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)$