Metamath Proof Explorer


Theorem 2wlkdlem2

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 }

Proof

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 }