Metamath Proof Explorer


Theorem 2wlkdlem2

Description: Lemma 2 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
Assertion 2wlkdlem2 ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 }

Proof

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 }