Description: Lemma 2 for 2wlkd . (Contributed by AV, 14-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2wlkd.p | |- P = <" A B C "> |
|
2wlkd.f | |- F = <" J K "> |
||
Assertion | 2wlkdlem2 | |- ( 0 ..^ ( # ` F ) ) = { 0 , 1 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2wlkd.p | |- P = <" A B C "> |
|
2 | 2wlkd.f | |- F = <" J K "> |
|
3 | 2 | fveq2i | |- ( # ` F ) = ( # ` <" J K "> ) |
4 | s2len | |- ( # ` <" J K "> ) = 2 |
|
5 | 3 4 | eqtri | |- ( # ` F ) = 2 |
6 | 5 | oveq2i | |- ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) |
7 | fzo0to2pr | |- ( 0 ..^ 2 ) = { 0 , 1 } |
|
8 | 6 7 | eqtri | |- ( 0 ..^ ( # ` F ) ) = { 0 , 1 } |