Description: Lemma 1 for wlk2v2e : F is a length 2 word of over { 0 } , the domain of the singleton word I . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wlk2v2e.i | |
|
wlk2v2e.f | |
||
Assertion | wlk2v2elem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlk2v2e.i | |
|
2 | wlk2v2e.f | |
|
3 | c0ex | |
|
4 | 3 | snid | |
5 | id | |
|
6 | 5 5 | s2cld | |
7 | 4 6 | ax-mp | |
8 | 1 | dmeqi | |
9 | s1dm | |
|
10 | 8 9 | eqtri | |
11 | 10 | wrdeqi | |
12 | 7 2 11 | 3eltr4i | |