Description: Lemma 2 for 2wlkd . (Contributed by AV, 14-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2wlkd.p | ⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 | |
2wlkd.f | ⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 | ||
Assertion | 2wlkdlem2 | ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2wlkd.p | ⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 | |
2 | 2wlkd.f | ⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 | |
3 | 2 | fveq2i | ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) |
4 | s2len | ⊢ ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) = 2 | |
5 | 3 4 | eqtri | ⊢ ( ♯ ‘ 𝐹 ) = 2 |
6 | 5 | oveq2i | ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) |
7 | fzo0to2pr | ⊢ ( 0 ..^ 2 ) = { 0 , 1 } | |
8 | 6 7 | eqtri | ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } |