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 ⊢V=Vtx⁡G
Assertion isspthonpth ⊢A∈V∧B∈V∧F∈W∧P∈Z→FASPathsOn⁡GBP↔FSPaths⁡GP∧P⁡0=A∧P⁡F=B

Proof

Step Hyp Ref Expression
1 isspthonpth.v ⊢V=Vtx⁡G
2 1 isspthson ⊢A∈V∧B∈V∧F∈W∧P∈Z→FASPathsOn⁡GBP↔FATrailsOn⁡GBP∧FSPaths⁡GP
3 1 istrlson ⊢A∈V∧B∈V∧F∈W∧P∈Z→FATrailsOn⁡GBP↔FAWalksOn⁡GBP∧FTrails⁡GP
4 3 adantr ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FATrailsOn⁡GBP↔FAWalksOn⁡GBP∧FTrails⁡GP
5 spthispth ⊢FSPaths⁡GP→FPaths⁡GP
6 pthistrl ⊢FPaths⁡GP→FTrails⁡GP
7 5 6 syl ⊢FSPaths⁡GP→FTrails⁡GP
8 7 adantl ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FTrails⁡GP
9 8 biantrud ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FAWalksOn⁡GBP↔FAWalksOn⁡GBP∧FTrails⁡GP
10 spthiswlk ⊢FSPaths⁡GP→FWalks⁡GP
11 10 adantl ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FWalks⁡GP
12 1 iswlkon ⊢A∈V∧B∈V∧F∈W∧P∈Z→FAWalksOn⁡GBP↔FWalks⁡GP∧P⁡0=A∧P⁡F=B
13 3anass ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B↔FWalks⁡GP∧P⁡0=A∧P⁡F=B
14 12 13 bitrdi ⊢A∈V∧B∈V∧F∈W∧P∈Z→FAWalksOn⁡GBP↔FWalks⁡GP∧P⁡0=A∧P⁡F=B
15 14 adantr ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FAWalksOn⁡GBP↔FWalks⁡GP∧P⁡0=A∧P⁡F=B
16 11 15 mpbirand ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FAWalksOn⁡GBP↔P⁡0=A∧P⁡F=B
17 4 9 16 3bitr2d ⊢A∈V∧B∈V∧F∈W∧P∈Z∧FSPaths⁡GP→FATrailsOn⁡GBP↔P⁡0=A∧P⁡F=B
18 17 ex ⊢A∈V∧B∈V∧F∈W∧P∈Z→FSPaths⁡GP→FATrailsOn⁡GBP↔P⁡0=A∧P⁡F=B
19 18 pm5.32rd ⊢A∈V∧B∈V∧F∈W∧P∈Z→FATrailsOn⁡GBP∧FSPaths⁡GP↔P⁡0=A∧P⁡F=B∧FSPaths⁡GP
20 3anass ⊢FSPaths⁡GP∧P⁡0=A∧P⁡F=B↔FSPaths⁡GP∧P⁡0=A∧P⁡F=B
21 ancom ⊢FSPaths⁡GP∧P⁡0=A∧P⁡F=B↔P⁡0=A∧P⁡F=B∧FSPaths⁡GP
22 20 21 bitr2i ⊢P⁡0=A∧P⁡F=B∧FSPaths⁡GP↔FSPaths⁡GP∧P⁡0=A∧P⁡F=B
23 19 22 bitrdi ⊢A∈V∧B∈V∧F∈W∧P∈Z→FATrailsOn⁡GBP∧FSPaths⁡GP↔FSPaths⁡GP∧P⁡0=A∧P⁡F=B
24 2 23 bitrd ⊢A∈V∧B∈V∧F∈W∧P∈Z→FASPathsOn⁡GBP↔FSPaths⁡GP∧P⁡0=A∧P⁡F=B