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 = f p | f Walks ⁡ G p ∧ Fun ⁡ p -1

Proof

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