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 | |- I = <" { X , Y } "> |
|
| wlk2v2e.f | |- F = <" 0 0 "> |
||
| Assertion | wlk2v2elem1 | |- F e. Word dom I |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlk2v2e.i | |- I = <" { X , Y } "> |
|
| 2 | wlk2v2e.f | |- F = <" 0 0 "> |
|
| 3 | c0ex | |- 0 e. _V |
|
| 4 | 3 | snid | |- 0 e. { 0 } |
| 5 | id | |- ( 0 e. { 0 } -> 0 e. { 0 } ) |
|
| 6 | 5 5 | s2cld | |- ( 0 e. { 0 } -> <" 0 0 "> e. Word { 0 } ) |
| 7 | 4 6 | ax-mp | |- <" 0 0 "> e. Word { 0 } |
| 8 | 1 | dmeqi | |- dom I = dom <" { X , Y } "> |
| 9 | s1dm | |- dom <" { X , Y } "> = { 0 } |
|
| 10 | 8 9 | eqtri | |- dom I = { 0 } |
| 11 | 10 | wrdeqi | |- Word dom I = Word { 0 } |
| 12 | 7 2 11 | 3eltr4i | |- F e. Word dom I |