Metamath Proof Explorer


Theorem isupwlkg

Description: Generalization of isupwlk : Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021)

Ref Expression
Hypotheses upwlksfval.v V = Vtx G
upwlksfval.i I = iEdg G
Assertion isupwlkg G W F UPWalks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1

Proof

Step Hyp Ref Expression
1 upwlksfval.v V = Vtx G
2 upwlksfval.i I = iEdg G
3 1 2 upwlksfval G V UPWalks G = f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
4 3 brfvopab F UPWalks G P G V F V P V
5 4 a1i G W F UPWalks G P G V F V P V
6 elex G W G V
7 elex F Word dom I F V
8 ovex 0 F V
9 1 fvexi V V
10 8 9 fpm P : 0 F V P V 𝑝𝑚 0 F
11 10 elexd P : 0 F V P V
12 7 11 anim12i F Word dom I P : 0 F V F V P V
13 12 3adant3 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 F V P V
14 6 13 anim12i G W F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 G V F V P V
15 14 ex G W F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 G V F V P V
16 3anass G V F V P V G V F V P V
17 15 16 syl6ibr G W F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 G V F V P V
18 1 2 isupwlk G V F V P V F UPWalks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
19 18 a1i G W G V F V P V F UPWalks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
20 5 17 19 pm5.21ndd G W F UPWalks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1