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	$$⊢\left(0..^\left|F\right|\right)=\left\{0,1,2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	$$⊢P=⟨“ABCD”⟩$$
2		3wlkd.f	$$⊢F=⟨“JKL”⟩$$
3	2	fveq2i	$$⊢\left|F\right|=\left|⟨“JKL”⟩\right|$$
4		s3len	$$⊢\left|⟨“JKL”⟩\right|=3$$
5	3 4	eqtri	$$⊢\left|F\right|=3$$
6	5	oveq2i	$$⊢\left(0..^\left|F\right|\right)=\left(0..^3\right)$$
7		fzo0to3tp	$$⊢\left(0..^3\right)=\left\{0,1,2\right\}$$
8	6 7	eqtri	$$⊢\left(0..^\left|F\right|\right)=\left\{0,1,2\right\}$$