Metamath Proof Explorer

Theorem upgrwlkdvspth

Description: A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by Alexander van der Vekens, 27-Oct-2017) (Revised by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvspth ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F SPaths ⁡ G P

Proof

Step Hyp Ref Expression
1 3simpc ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F Walks ⁡ G P ∧ Fun ⁡ P -1
2 upgrspthswlk ⊢ G ∈ UPGraph → SPaths ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ p -1
3 2 3ad2ant1 ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → SPaths ⁡ G = f p | f Walks ⁡ G p ∧ Fun ⁡ p -1
4 3 breqd ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F SPaths ⁡ G P ↔ F f p | f Walks ⁡ G p ∧ Fun ⁡ p -1 P
5 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
6 3simpc ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ V ∧ P ∈ V
7 5 6 syl ⊢ F Walks ⁡ G P → F ∈ V ∧ P ∈ V
8 7 3ad2ant2 ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F ∈ V ∧ P ∈ V
9 breq12 ⊢ f = F ∧ p = P → f Walks ⁡ G p ↔ F Walks ⁡ G P
10 cnveq ⊢ p = P → p -1 = P -1
11 10 funeqd ⊢ p = P → Fun ⁡ p -1 ↔ Fun ⁡ P -1
12 11 adantl ⊢ f = F ∧ p = P → Fun ⁡ p -1 ↔ Fun ⁡ P -1
13 9 12 anbi12d ⊢ f = F ∧ p = P → f Walks ⁡ G p ∧ Fun ⁡ p -1 ↔ F Walks ⁡ G P ∧ Fun ⁡ P -1
14 eqid ⊢ f p | f Walks ⁡ G p ∧ Fun ⁡ p -1 = f p | f Walks ⁡ G p ∧ Fun ⁡ p -1
15 13 14 brabga ⊢ F ∈ V ∧ P ∈ V → F f p | f Walks ⁡ G p ∧ Fun ⁡ p -1 P ↔ F Walks ⁡ G P ∧ Fun ⁡ P -1
16 8 15 syl ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F f p | f Walks ⁡ G p ∧ Fun ⁡ p -1 P ↔ F Walks ⁡ G P ∧ Fun ⁡ P -1
17 4 16 bitrd ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F SPaths ⁡ G P ↔ F Walks ⁡ G P ∧ Fun ⁡ P -1
18 1 17 mpbird ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P ∧ Fun ⁡ P -1 → F SPaths ⁡ G P