Metamath Proof Explorer

Theorem upgrspthswlk

Description: The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p_0, p_1, p_2 } be a hyperedge, then ( p_0, e, p_1, e, p_2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021) (Proof shortened by AV, 17-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion upgrspthswlk ⊢G∈UPGraph→SPaths⁡G=fp|fWalks⁡Gp∧Fun⁡p-1

Proof

Step Hyp Ref Expression
1 spthsfval ⊢SPaths⁡G=fp|fTrails⁡Gp∧Fun⁡p-1
2 istrl ⊢fTrails⁡Gp↔fWalks⁡Gp∧Fun⁡f-1
3 upgrwlkdvde ⊢G∈UPGraph∧fWalks⁡Gp∧Fun⁡p-1→Fun⁡f-1
4 3 3exp ⊢G∈UPGraph→fWalks⁡Gp→Fun⁡p-1→Fun⁡f-1
5 4 com23 ⊢G∈UPGraph→Fun⁡p-1→fWalks⁡Gp→Fun⁡f-1
6 5 imp ⊢G∈UPGraph∧Fun⁡p-1→fWalks⁡Gp→Fun⁡f-1
7 6 pm4.71d ⊢G∈UPGraph∧Fun⁡p-1→fWalks⁡Gp↔fWalks⁡Gp∧Fun⁡f-1
8 2 7 bitr4id ⊢G∈UPGraph∧Fun⁡p-1→fTrails⁡Gp↔fWalks⁡Gp
9 8 ex ⊢G∈UPGraph→Fun⁡p-1→fTrails⁡Gp↔fWalks⁡Gp
10 9 pm5.32rd ⊢G∈UPGraph→fTrails⁡Gp∧Fun⁡p-1↔fWalks⁡Gp∧Fun⁡p-1
11 10 opabbidv ⊢G∈UPGraph→fp|fTrails⁡Gp∧Fun⁡p-1=fp|fWalks⁡Gp∧Fun⁡p-1
12 1 11 eqtrid ⊢G∈UPGraph→SPaths⁡G=fp|fWalks⁡Gp∧Fun⁡p-1