Metamath Proof Explorer

Theorem spthispth

Description: A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion spthispth 
|- ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> F ( Trails ` G ) P )
2 funres11 
 |-  ( Fun `' P -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
3 2 adantl 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
4 imain 
 |-  ( Fun `' P -> ( P " ( { 0 , ( # ` F ) } i^i ( 1 ..^ ( # ` F ) ) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) )
5 1e0p1 
 |-  1 = ( 0 + 1 )
6 5 oveq1i 
 |-  ( 1 ..^ ( # ` F ) ) = ( ( 0 + 1 ) ..^ ( # ` F ) )
7 6 ineq2i 
 |-  ( { 0 , ( # ` F ) } i^i ( 1 ..^ ( # ` F ) ) ) = ( { 0 , ( # ` F ) } i^i ( ( 0 + 1 ) ..^ ( # ` F ) ) )
8 0z 
 |-  0 e. ZZ
9 prinfzo0 
 |-  ( 0 e. ZZ -> ( { 0 , ( # ` F ) } i^i ( ( 0 + 1 ) ..^ ( # ` F ) ) ) = (/) )
10 8 9 ax-mp 
 |-  ( { 0 , ( # ` F ) } i^i ( ( 0 + 1 ) ..^ ( # ` F ) ) ) = (/)
11 7 10 eqtri 
 |-  ( { 0 , ( # ` F ) } i^i ( 1 ..^ ( # ` F ) ) ) = (/)
12 11 imaeq2i 
 |-  ( P " ( { 0 , ( # ` F ) } i^i ( 1 ..^ ( # ` F ) ) ) ) = ( P " (/) )
13 ima0 
 |-  ( P " (/) ) = (/)
14 12 13 eqtri 
 |-  ( P " ( { 0 , ( # ` F ) } i^i ( 1 ..^ ( # ` F ) ) ) ) = (/)
15 4 14 eqtr3di 
 |-  ( Fun `' P -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
16 15 adantl 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
17 1 3 16 3jca 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
18 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
19 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
20 17 18 19 3imtr4i 
 |-  ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )