# 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}=\mathrm{Vtx}\left({G}\right)$
Assertion isspthonpth ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{SPathsOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 isspthonpth.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 1 isspthson ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{SPathsOn}\left({G}\right){B}\right){P}↔\left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\right)$
3 1 istrlson ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}↔\left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\right)$
4 3 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to \left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}↔\left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\right)$
5 spthispth ${⊢}{F}\mathrm{SPaths}\left({G}\right){P}\to {F}\mathrm{Paths}\left({G}\right){P}$
6 pthistrl ${⊢}{F}\mathrm{Paths}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
7 5 6 syl ${⊢}{F}\mathrm{SPaths}\left({G}\right){P}\to {F}\mathrm{Trails}\left({G}\right){P}$
8 7 adantl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to {F}\mathrm{Trails}\left({G}\right){P}$
9 8 biantrud ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\right)$
10 spthiswlk ${⊢}{F}\mathrm{SPaths}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
11 10 adantl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to {F}\mathrm{Walks}\left({G}\right){P}$
12 1 iswlkon ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
13 3anass ${⊢}\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
14 12 13 syl6bb ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)\right)$
15 14 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)\right)$
16 11 15 mpbirand ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
17 4 9 16 3bitr2d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\to \left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}↔\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
18 17 ex ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\mathrm{SPaths}\left({G}\right){P}\to \left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}↔\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)\right)$
19 18 pm5.32rd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left(\left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)↔\left(\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)\right)$
20 3anass ${⊢}\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)↔\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge \left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
21 ancom ${⊢}\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge \left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)↔\left(\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)$
22 20 21 bitr2i ${⊢}\left(\left({P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)↔\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)$
23 19 22 syl6bb ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left(\left({F}\left({A}\mathrm{TrailsOn}\left({G}\right){B}\right){P}\wedge {F}\mathrm{SPaths}\left({G}\right){P}\right)↔\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
24 2 23 bitrd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {W}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{SPathsOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{SPaths}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$