Metamath Proof Explorer


Theorem upgrwlkdvde

Description: In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvde G UPGraph F Walks G P Fun P -1 Fun F -1

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 eqid iEdg G = iEdg G
3 1 2 upgriswlk G UPGraph F Walks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
4 df-f1 P : 0 F 1-1 Vtx G P : 0 F Vtx G Fun P -1
5 4 simplbi2 P : 0 F Vtx G Fun P -1 P : 0 F 1-1 Vtx G
6 5 3ad2ant2 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 Fun P -1 P : 0 F 1-1 Vtx G
7 6 impcom Fun P -1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 P : 0 F 1-1 Vtx G
8 simpr1 Fun P -1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 F Word dom iEdg G
9 7 8 jca Fun P -1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 P : 0 F 1-1 Vtx G F Word dom iEdg G
10 simpr3 Fun P -1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 k 0 ..^ F iEdg G F k = P k P k + 1
11 upgrwlkdvdelem P : 0 F 1-1 Vtx G F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 Fun F -1
12 9 10 11 sylc Fun P -1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 Fun F -1
13 12 expcom F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 Fun P -1 Fun F -1
14 3 13 syl6bi G UPGraph F Walks G P Fun P -1 Fun F -1
15 14 3imp G UPGraph F Walks G P Fun P -1 Fun F -1