This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) 𝑃 )