Theorem s3fn

Description: A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017) (Revised by AV, 23-Jan-2021)

	Ref	Expression
Assertion	s3fn	$$⊢\left(A\in V\wedge B\in V\wedge C\in V\right)\to ⟨“ABC”⟩Fn\left\{0,1,2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		s3cl	$$⊢\left(A\in V\wedge B\in V\wedge C\in V\right)\to ⟨“ABC”⟩\in \mathrm{Word}V$$
2		wrdfn	$$⊢⟨“ABC”⟩\in \mathrm{Word}V\to ⟨“ABC”⟩Fn\left(0..^\left|⟨“ABC”⟩\right|\right)$$
3	1 2	syl	$$⊢\left(A\in V\wedge B\in V\wedge C\in V\right)\to ⟨“ABC”⟩Fn\left(0..^\left|⟨“ABC”⟩\right|\right)$$
4		s3len	$$⊢\left|⟨“ABC”⟩\right|=3$$
5	4	oveq2i	$$⊢\left(0..^\left|⟨“ABC”⟩\right|\right)=\left(0..^3\right)$$
6		fzo0to3tp	$$⊢\left(0..^3\right)=\left\{0,1,2\right\}$$
7	5 6	eqtr2i	$$⊢\left\{0,1,2\right\}=\left(0..^\left|⟨“ABC”⟩\right|\right)$$
8	7	fneq2i	$$⊢⟨“ABC”⟩Fn\left\{0,1,2\right\}\leftrightarrow ⟨“ABC”⟩Fn\left(0..^\left|⟨“ABC”⟩\right|\right)$$
9	3 8	sylibr	$$⊢\left(A\in V\wedge B\in V\wedge C\in V\right)\to ⟨“ABC”⟩Fn\left\{0,1,2\right\}$$