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	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐹 ( Cycles ‘ 𝑆 ) 𝑃 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		subgrpth	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐹 ( Paths ‘ 𝑆 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) )
2	1	anim1d	⊢ ( 𝑆 SubGraph 𝐺 → ( ( 𝐹 ( Paths ‘ 𝑆 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
3		iscycl	⊢ ( 𝐹 ( Cycles ‘ 𝑆 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝑆 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4		iscycl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
5	2 3 4	3imtr4g	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐹 ( Cycles ‘ 𝑆 ) 𝑃 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) )