Metamath Proof Explorer


Theorem ewlksfval

Description: The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i I=iEdgG
Assertion ewlksfval GWS0*GEdgWalksS=f|fWorddomIk1..^fSIfk1Ifk

Proof

Step Hyp Ref Expression
1 ewlksfval.i I=iEdgG
2 df-ewlks EdgWalks=gV,s0*f|[˙iEdgg/i]˙fWorddomik1..^fsifk1ifk
3 2 a1i GWS0*EdgWalks=gV,s0*f|[˙iEdgg/i]˙fWorddomik1..^fsifk1ifk
4 fvexd g=Gs=SiEdggV
5 simpr g=Gs=Si=iEdggi=iEdgg
6 fveq2 g=GiEdgg=iEdgG
7 6 adantr g=Gs=SiEdgg=iEdgG
8 7 adantr g=Gs=Si=iEdggiEdgg=iEdgG
9 5 8 eqtrd g=Gs=Si=iEdggi=iEdgG
10 9 dmeqd g=Gs=Si=iEdggdomi=domiEdgG
11 wrdeq domi=domiEdgGWorddomi=WorddomiEdgG
12 10 11 syl g=Gs=Si=iEdggWorddomi=WorddomiEdgG
13 12 eleq2d g=Gs=Si=iEdggfWorddomifWorddomiEdgG
14 simpr g=Gs=Ss=S
15 14 adantr g=Gs=Si=iEdggs=S
16 9 fveq1d g=Gs=Si=iEdggifk1=iEdgGfk1
17 9 fveq1d g=Gs=Si=iEdggifk=iEdgGfk
18 16 17 ineq12d g=Gs=Si=iEdggifk1ifk=iEdgGfk1iEdgGfk
19 18 fveq2d g=Gs=Si=iEdggifk1ifk=iEdgGfk1iEdgGfk
20 15 19 breq12d g=Gs=Si=iEdggsifk1ifkSiEdgGfk1iEdgGfk
21 20 ralbidv g=Gs=Si=iEdggk1..^fsifk1ifkk1..^fSiEdgGfk1iEdgGfk
22 13 21 anbi12d g=Gs=Si=iEdggfWorddomik1..^fsifk1ifkfWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
23 4 22 sbcied g=Gs=S[˙iEdgg/i]˙fWorddomik1..^fsifk1ifkfWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
24 23 abbidv g=Gs=Sf|[˙iEdgg/i]˙fWorddomik1..^fsifk1ifk=f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
25 24 adantl GWS0*g=Gs=Sf|[˙iEdgg/i]˙fWorddomik1..^fsifk1ifk=f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
26 elex GWGV
27 26 adantr GWS0*GV
28 simpr GWS0*S0*
29 df-rab fWorddomiEdgG|k1..^fSiEdgGfk1iEdgGfk=f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
30 fvex iEdgGV
31 30 dmex domiEdgGV
32 31 wrdexi WorddomiEdgGV
33 32 rabex fWorddomiEdgG|k1..^fSiEdgGfk1iEdgGfkV
34 33 a1i GWS0*fWorddomiEdgG|k1..^fSiEdgGfk1iEdgGfkV
35 29 34 eqeltrrid GWS0*f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfkV
36 3 25 27 28 35 ovmpod GWS0*GEdgWalksS=f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk
37 1 eqcomi iEdgG=I
38 37 a1i GWS0*iEdgG=I
39 38 dmeqd GWS0*domiEdgG=domI
40 wrdeq domiEdgG=domIWorddomiEdgG=WorddomI
41 39 40 syl GWS0*WorddomiEdgG=WorddomI
42 41 eleq2d GWS0*fWorddomiEdgGfWorddomI
43 38 fveq1d GWS0*iEdgGfk1=Ifk1
44 38 fveq1d GWS0*iEdgGfk=Ifk
45 43 44 ineq12d GWS0*iEdgGfk1iEdgGfk=Ifk1Ifk
46 45 fveq2d GWS0*iEdgGfk1iEdgGfk=Ifk1Ifk
47 46 breq2d GWS0*SiEdgGfk1iEdgGfkSIfk1Ifk
48 47 ralbidv GWS0*k1..^fSiEdgGfk1iEdgGfkk1..^fSIfk1Ifk
49 42 48 anbi12d GWS0*fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfkfWorddomIk1..^fSIfk1Ifk
50 49 abbidv GWS0*f|fWorddomiEdgGk1..^fSiEdgGfk1iEdgGfk=f|fWorddomIk1..^fSIfk1Ifk
51 36 50 eqtrd GWS0*GEdgWalksS=f|fWorddomIk1..^fSIfk1Ifk