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 | |
|
wwlksnextprop.e | |
||
wwlksnextprop.y | |
||
Assertion | disjxwwlkn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wwlksnextprop.x | |
|
2 | wwlksnextprop.e | |
|
3 | wwlksnextprop.y | |
|
4 | simp1 | |
|
5 | 4 | rgenw | |
6 | ss2rab | |
|
7 | 5 6 | mpbir | |
8 | wwlkssswwlksn | |
|
9 | eqid | |
|
10 | 9 | wwlkssswrd | |
11 | 8 10 | sstri | |
12 | 1 11 | eqsstri | |
13 | rabss2 | |
|
14 | 12 13 | ax-mp | |
15 | 7 14 | sstri | |
16 | 15 | rgenw | |
17 | disjwrdpfx | |
|
18 | disjss2 | |
|
19 | 16 17 18 | mp2 | |