Metamath Proof Explorer


Theorem isewlk

Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i I=iEdgG
Assertion isewlk GWS0*FUFGEdgWalksSFWorddomIk1..^FSIFk1IFk

Proof

Step Hyp Ref Expression
1 ewlksfval.i I=iEdgG
2 1 ewlksfval GWS0*GEdgWalksS=f|fWorddomIk1..^fSIfk1Ifk
3 2 3adant3 GWS0*FUGEdgWalksS=f|fWorddomIk1..^fSIfk1Ifk
4 3 eleq2d GWS0*FUFGEdgWalksSFf|fWorddomIk1..^fSIfk1Ifk
5 eleq1 f=FfWorddomIFWorddomI
6 fveq2 f=Ff=F
7 6 oveq2d f=F1..^f=1..^F
8 fveq1 f=Ffk1=Fk1
9 8 fveq2d f=FIfk1=IFk1
10 fveq1 f=Ffk=Fk
11 10 fveq2d f=FIfk=IFk
12 9 11 ineq12d f=FIfk1Ifk=IFk1IFk
13 12 fveq2d f=FIfk1Ifk=IFk1IFk
14 13 breq2d f=FSIfk1IfkSIFk1IFk
15 7 14 raleqbidv f=Fk1..^fSIfk1Ifkk1..^FSIFk1IFk
16 5 15 anbi12d f=FfWorddomIk1..^fSIfk1IfkFWorddomIk1..^FSIFk1IFk
17 16 elabg FUFf|fWorddomIk1..^fSIfk1IfkFWorddomIk1..^FSIFk1IFk
18 17 3ad2ant3 GWS0*FUFf|fWorddomIk1..^fSIfk1IfkFWorddomIk1..^FSIFk1IFk
19 4 18 bitrd GWS0*FUFGEdgWalksSFWorddomIk1..^FSIFk1IFk