Metamath Proof Explorer


Theorem 3wlkdlem2

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

Ref Expression
Hypotheses 3wlkd.p P = ⟨“ ABCD ”⟩
3wlkd.f F = ⟨“ JKL ”⟩
Assertion 3wlkdlem2 0 ..^ F = 0 1 2

Proof

Step Hyp Ref Expression
1 3wlkd.p P = ⟨“ ABCD ”⟩
2 3wlkd.f F = ⟨“ JKL ”⟩
3 2 fveq2i F = ⟨“ JKL ”⟩
4 s3len ⟨“ JKL ”⟩ = 3
5 3 4 eqtri F = 3
6 5 oveq2i 0 ..^ F = 0 ..^ 3
7 fzo0to3tp 0 ..^ 3 = 0 1 2
8 6 7 eqtri 0 ..^ F = 0 1 2