# Metamath Proof Explorer

## Theorem ispth

Description: Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 pthsfval ${⊢}\mathrm{Paths}\left({G}\right)=\left\{⟨{f},{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)\right\}$
2 3anass ${⊢}\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)↔\left({f}\mathrm{Trails}\left({G}\right){p}\wedge \left(\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)\right)$
3 2 opabbii ${⊢}\left\{⟨{f},{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)\right\}=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge \left(\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)\right)\right\}$
4 1 3 eqtri ${⊢}\mathrm{Paths}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge \left(\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)\right)\right\}$
5 simpr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}={P}$
6 fveq2 ${⊢}{f}={F}\to \left|{f}\right|=\left|{F}\right|$
7 6 oveq2d ${⊢}{f}={F}\to \left(1..^\left|{f}\right|\right)=\left(1..^\left|{F}\right|\right)$
8 7 adantr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left(1..^\left|{f}\right|\right)=\left(1..^\left|{F}\right|\right)$
9 5 8 reseq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {{p}↾}_{\left(1..^\left|{f}\right|\right)}={{P}↾}_{\left(1..^\left|{F}\right|\right)}$
10 9 cnveqd ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {\left({{p}↾}_{\left(1..^\left|{f}\right|\right)}\right)}^{-1}={\left({{P}↾}_{\left(1..^\left|{F}\right|\right)}\right)}^{-1}$
11 10 funeqd ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left(\mathrm{Fun}{\left({{p}↾}_{\left(1..^\left|{f}\right|\right)}\right)}^{-1}↔\mathrm{Fun}{\left({{P}↾}_{\left(1..^\left|{F}\right|\right)}\right)}^{-1}\right)$
12 6 preq2d ${⊢}{f}={F}\to \left\{0,\left|{f}\right|\right\}=\left\{0,\left|{F}\right|\right\}$
13 12 adantr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left\{0,\left|{f}\right|\right\}=\left\{0,\left|{F}\right|\right\}$
14 5 13 imaeq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left[\left\{0,\left|{f}\right|\right\}\right]={P}\left[\left\{0,\left|{F}\right|\right\}\right]$
15 5 8 imaeq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left[\left(1..^\left|{f}\right|\right)\right]={P}\left[\left(1..^\left|{F}\right|\right)\right]$
16 14 15 ineq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left[\left\{0,\left|{f}\right|\right\}\right]\cap {p}\left[\left(1..^\left|{f}\right|\right)\right]={P}\left[\left\{0,\left|{F}\right|\right\}\right]\cap {P}\left[\left(1..^\left|{F}\right|\right)\right]$
17 16 eqeq1d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({p}\left[\left\{0,\left|{f}\right|\right\}\right]\cap {p}\left[\left(1..^\left|{f}\right|\right)\right]=\varnothing ↔{P}\left[\left\{0,\left|{F}\right|\right\}\right]\cap {P}\left[\left(1..^\left|{F}\right|\right)\right]=\varnothing \right)$
18 11 17 anbi12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left(\left(\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)↔\left(\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)\right)$
19 reltrls ${⊢}\mathrm{Rel}\mathrm{Trails}\left({G}\right)$
20 4 18 19 brfvopabrbr ${⊢}{F}\mathrm{Paths}\left({G}\right){P}↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge \left(\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)\right)$
21 3anass ${⊢}\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)↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge \left(\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)\right)$
22 20 21 bitr4i ${⊢}{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)$