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 ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun 𝑃 ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
2 funres11 ( Fun 𝑃 → Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
3 2 adantl ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun 𝑃 ) → Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
4 imain ( Fun 𝑃 → ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
5 1e0p1 1 = ( 0 + 1 )
6 5 oveq1i ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) )
7 6 ineq2i ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) )
8 0z 0 ∈ ℤ
9 prinfzo0 ( 0 ∈ ℤ → ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅ )
10 8 9 ax-mp ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
11 7 10 eqtri ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
12 11 imaeq2i ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( 𝑃 “ ∅ )
13 ima0 ( 𝑃 “ ∅ ) = ∅
14 12 13 eqtri ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅
15 4 14 eqtr3di ( Fun 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
16 15 adantl ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun 𝑃 ) → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
17 1 3 16 3jca ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun 𝑃 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
18 isspth ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun 𝑃 ) )
19 ispth ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
20 17 18 19 3imtr4i ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃𝐹 ( Paths ‘ 𝐺 ) 𝑃 )