Metamath Proof Explorer

Theorem isspthonpth

Description: A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-Jan-2021)

Ref Expression
Hypothesis isspthonpth.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion isspthonpth ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 isspthonpth.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 isspthson ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )
3 1 istrlson ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
4 3 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
5 spthispth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
6 pthistrl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
7 5 6 syl ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
8 7 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
9 8 biantrud ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
10 spthiswlk ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
11 10 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
12 1 iswlkon ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
13 3anass ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
14 12 13 bitrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) )
15 14 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) )
16 11 15 mpbirand ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
17 4 9 16 3bitr2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
18 17 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) )
19 18 pm5.32rd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ) )
20 3anass ⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
21 ancom ⊢ ( ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) )
22 20 21 bitr2i ⊢ ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) )
23 19 22 bitrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ∧ 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )
24 2 23 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) )