Metamath Proof Explorer


Theorem disjxwwlkn

Description: Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x X=N+1WWalksNG
wwlksnextprop.e E=EdgG
wwlksnextprop.y Y=wNWWalksNG|w0=P
Assertion disjxwwlkn DisjyYxX|xprefixM=yy0=PlastSylastSxE

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x X=N+1WWalksNG
2 wwlksnextprop.e E=EdgG
3 wwlksnextprop.y Y=wNWWalksNG|w0=P
4 simp1 xprefixM=yy0=PlastSylastSxExprefixM=y
5 4 rgenw xXxprefixM=yy0=PlastSylastSxExprefixM=y
6 ss2rab xX|xprefixM=yy0=PlastSylastSxExX|xprefixM=yxXxprefixM=yy0=PlastSylastSxExprefixM=y
7 5 6 mpbir xX|xprefixM=yy0=PlastSylastSxExX|xprefixM=y
8 wwlkssswwlksn N+1WWalksNGWWalksG
9 eqid VtxG=VtxG
10 9 wwlkssswrd WWalksGWordVtxG
11 8 10 sstri N+1WWalksNGWordVtxG
12 1 11 eqsstri XWordVtxG
13 rabss2 XWordVtxGxX|xprefixM=yxWordVtxG|xprefixM=y
14 12 13 ax-mp xX|xprefixM=yxWordVtxG|xprefixM=y
15 7 14 sstri xX|xprefixM=yy0=PlastSylastSxExWordVtxG|xprefixM=y
16 15 rgenw yYxX|xprefixM=yy0=PlastSylastSxExWordVtxG|xprefixM=y
17 disjwrdpfx DisjyYxWordVtxG|xprefixM=y
18 disjss2 yYxX|xprefixM=yy0=PlastSylastSxExWordVtxG|xprefixM=yDisjyYxWordVtxG|xprefixM=yDisjyYxX|xprefixM=yy0=PlastSylastSxE
19 16 17 18 mp2 DisjyYxX|xprefixM=yy0=PlastSylastSxE