Metamath Proof Explorer

Theorem subgrcycl

Description: If a cycle exists in a subgraph of a graph G , then that cycle also exists in G . (Contributed by BTernaryTau, 23-Oct-2023)

Ref Expression
Assertion subgrcycl 
|- ( S SubGraph G -> ( F ( Cycles ` S ) P -> F ( Cycles ` G ) P ) )

Proof

Step Hyp Ref Expression
1 subgrpth 
 |-  ( S SubGraph G -> ( F ( Paths ` S ) P -> F ( Paths ` G ) P ) )
2 1 anim1d 
 |-  ( S SubGraph G -> ( ( F ( Paths ` S ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
3 iscycl 
 |-  ( F ( Cycles ` S ) P <-> ( F ( Paths ` S ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
5 2 3 4 3imtr4g 
 |-  ( S SubGraph G -> ( F ( Cycles ` S ) P -> F ( Cycles ` G ) P ) )