# Metamath Proof Explorer

## Theorem 1pthd

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses 1wlkd.p ${⊢}{P}=⟨“{X}{Y}”⟩$
1wlkd.f ${⊢}{F}=⟨“{J}”⟩$
1wlkd.x ${⊢}{\phi }\to {X}\in {V}$
1wlkd.y ${⊢}{\phi }\to {Y}\in {V}$
1wlkd.l ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {I}\left({J}\right)=\left\{{X}\right\}$
1wlkd.j ${⊢}\left({\phi }\wedge {X}\ne {Y}\right)\to \left\{{X},{Y}\right\}\subseteq {I}\left({J}\right)$
1wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
1wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion 1pthd ${⊢}{\phi }\to {F}\mathrm{Paths}\left({G}\right){P}$

### Proof

Step Hyp Ref Expression
1 1wlkd.p ${⊢}{P}=⟨“{X}{Y}”⟩$
2 1wlkd.f ${⊢}{F}=⟨“{J}”⟩$
3 1wlkd.x ${⊢}{\phi }\to {X}\in {V}$
4 1wlkd.y ${⊢}{\phi }\to {Y}\in {V}$
5 1wlkd.l ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {I}\left({J}\right)=\left\{{X}\right\}$
6 1wlkd.j ${⊢}\left({\phi }\wedge {X}\ne {Y}\right)\to \left\{{X},{Y}\right\}\subseteq {I}\left({J}\right)$
7 1wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
8 1wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
9 1 2 3 4 5 6 7 8 1trld ${⊢}{\phi }\to {F}\mathrm{Trails}\left({G}\right){P}$
10 simpr ${⊢}\left({\phi }\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to {F}\mathrm{Trails}\left({G}\right){P}$
11 1 2 1pthdlem1 ${⊢}\mathrm{Fun}{\left({{P}↾}_{\left(1..^\left|{F}\right|\right)}\right)}^{-1}$
12 11 a1i ${⊢}\left({\phi }\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to \mathrm{Fun}{\left({{P}↾}_{\left(1..^\left|{F}\right|\right)}\right)}^{-1}$
13 1 2 1pthdlem2 ${⊢}{P}\left[\left\{0,\left|{F}\right|\right\}\right]\cap {P}\left[\left(1..^\left|{F}\right|\right)\right]=\varnothing$
14 13 a1i ${⊢}\left({\phi }\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to {P}\left[\left\{0,\left|{F}\right|\right\}\right]\cap {P}\left[\left(1..^\left|{F}\right|\right)\right]=\varnothing$
15 ispth ${⊢}{F}\mathrm{Paths}\left({G}\right){P}↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge \mathrm{Fun}{\left({{P}↾}_{\left(1..^\left|{F}\right|\right)}\right)}^{-1}\wedge {P}\left[\left\{0,\left|{F}\right|\right\}\right]\cap {P}\left[\left(1..^\left|{F}\right|\right)\right]=\varnothing \right)$
16 10 12 14 15 syl3anbrc ${⊢}\left({\phi }\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to {F}\mathrm{Paths}\left({G}\right){P}$
17 9 16 mpdan ${⊢}{\phi }\to {F}\mathrm{Paths}\left({G}\right){P}$