Metamath Proof Explorer

Theorem subgrpth

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

Ref Expression
Assertion subgrpth 
|- ( S SubGraph G -> ( F ( Paths ` S ) P -> F ( Paths ` G ) P ) )

Proof

Step Hyp Ref Expression
1 subgrtrl 
 |-  ( S SubGraph G -> ( F ( Trails ` S ) P -> F ( Trails ` G ) P ) )
2 idd 
 |-  ( S SubGraph G -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) )
3 idd 
 |-  ( S SubGraph G -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
4 1 2 3 3anim123d 
 |-  ( S SubGraph G -> ( ( F ( Trails ` S ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) )
5 ispth 
 |-  ( F ( Paths ` S ) P <-> ( F ( Trails ` S ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
6 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
7 4 5 6 3imtr4g 
 |-  ( S SubGraph G -> ( F ( Paths ` S ) P -> F ( Paths ` G ) P ) )