Metamath Proof Explorer

Theorem pthdepisspth

Description: A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 12-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion pthdepisspth ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 ispth ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
2 simplll ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
3 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
5 3 4 syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
6 5 ad3antrrr ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 7 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
9 3 8 syl ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
10 9 ad3antrrr ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
11 simpllr ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
12 simpr ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
13 10 11 12 3jca ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
14 simplr ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
15 injresinj ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ → Fun ◡ 𝑃 ) ) )
16 6 13 14 15 syl3c ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → Fun ◡ 𝑃 )
17 2 16 jca ⊢ ( ( ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
18 17 ex3 ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
19 1 18 sylbi ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
20 19 imp ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
21 isspth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
22 20 21 sylibr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )