Metamath Proof Explorer

Theorem subgrtrl

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

Ref Expression
Assertion subgrtrl 
|- ( S SubGraph G -> ( F ( Trails ` S ) P -> F ( Trails ` G ) P ) )

Proof

Step Hyp Ref Expression
1 subgrwlk 
 |-  ( S SubGraph G -> ( F ( Walks ` S ) P -> F ( Walks ` G ) P ) )
2 1 anim1d 
 |-  ( S SubGraph G -> ( ( F ( Walks ` S ) P /\ Fun `' F ) -> ( F ( Walks ` G ) P /\ Fun `' F ) ) )
3 istrl 
 |-  ( F ( Trails ` S ) P <-> ( F ( Walks ` S ) P /\ Fun `' F ) )
4 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
5 2 3 4 3imtr4g 
 |-  ( S SubGraph G -> ( F ( Trails ` S ) P -> F ( Trails ` G ) P ) )