Description: In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018) (Revised by AV, 5-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | usgr2pthspth | ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pthistrl | ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) | |
| 2 | usgr2trlspth | ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) | |
| 3 | 1 2 | syl5ib | ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) |
| 4 | spthispth | ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) | |
| 5 | 3 4 | impbid1 | ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) |