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∧FWalks⁡GP∧Fun⁡P-1→FSPaths⁡GP

Proof

Step Hyp Ref Expression
1 3simpc ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→FWalks⁡GP∧Fun⁡P-1
2 upgrspthswlk ⊢G∈UPGraph→SPaths⁡G=fp|fWalks⁡Gp∧Fun⁡p-1
3 2 3ad2ant1 ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→SPaths⁡G=fp|fWalks⁡Gp∧Fun⁡p-1
4 3 breqd ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→FSPaths⁡GP↔Ffp|fWalks⁡Gp∧Fun⁡p-1P
5 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
6 3simpc ⊢G∈V∧F∈V∧P∈V→F∈V∧P∈V
7 5 6 syl ⊢FWalks⁡GP→F∈V∧P∈V
8 7 3ad2ant2 ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→F∈V∧P∈V
9 breq12 ⊢f=F∧p=P→fWalks⁡Gp↔FWalks⁡GP
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→fWalks⁡Gp∧Fun⁡p-1↔FWalks⁡GP∧Fun⁡P-1
14 eqid ⊢fp|fWalks⁡Gp∧Fun⁡p-1=fp|fWalks⁡Gp∧Fun⁡p-1
15 13 14 brabga ⊢F∈V∧P∈V→Ffp|fWalks⁡Gp∧Fun⁡p-1P↔FWalks⁡GP∧Fun⁡P-1
16 8 15 syl ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→Ffp|fWalks⁡Gp∧Fun⁡p-1P↔FWalks⁡GP∧Fun⁡P-1
17 4 16 bitrd ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→FSPaths⁡GP↔FWalks⁡GP∧Fun⁡P-1
18 1 17 mpbird ⊢G∈UPGraph∧FWalks⁡GP∧Fun⁡P-1→FSPaths⁡GP