Theorem s3rn

Description: Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023)

	Ref	Expression
Hypotheses	s3rn.i	$$⊢\phi \to I\in D$$
	s3rn.j	$$⊢\phi \to J\in D$$
	s3rn.k	$$⊢\phi \to K\in D$$
Assertion	s3rn	$$⊢\phi \to \mathrm{ran}⟨“IJK”⟩=\left\{I,J,K\right\}$$

Proof

Step	Hyp	Ref	Expression
1		s3rn.i	$$⊢\phi \to I\in D$$
2		s3rn.j	$$⊢\phi \to J\in D$$
3		s3rn.k	$$⊢\phi \to K\in D$$
4		imadmrn	$$⊢⟨“IJK”⟩\left[\mathrm{dom}⟨“IJK”⟩\right]=\mathrm{ran}⟨“IJK”⟩$$
5	1 2 3	s3cld	$$⊢\phi \to ⟨“IJK”⟩\in \mathrm{Word}D$$
6		wrdfn	$$⊢⟨“IJK”⟩\in \mathrm{Word}D\to ⟨“IJK”⟩Fn\left(0..^\left|⟨“IJK”⟩\right|\right)$$
7		s3len	$$⊢\left|⟨“IJK”⟩\right|=3$$
8	7	oveq2i	$$⊢\left(0..^\left|⟨“IJK”⟩\right|\right)=\left(0..^3\right)$$
9		fzo0to3tp	$$⊢\left(0..^3\right)=\left\{0,1,2\right\}$$
10	8 9	eqtri	$$⊢\left(0..^\left|⟨“IJK”⟩\right|\right)=\left\{0,1,2\right\}$$
11	10	fneq2i	$$⊢⟨“IJK”⟩Fn\left(0..^\left|⟨“IJK”⟩\right|\right)\leftrightarrow ⟨“IJK”⟩Fn\left\{0,1,2\right\}$$
12	11	biimpi	$$⊢⟨“IJK”⟩Fn\left(0..^\left|⟨“IJK”⟩\right|\right)\to ⟨“IJK”⟩Fn\left\{0,1,2\right\}$$
13	5 6 12	3syl	$$⊢\phi \to ⟨“IJK”⟩Fn\left\{0,1,2\right\}$$
14	13	fndmd	$$⊢\phi \to \mathrm{dom}⟨“IJK”⟩=\left\{0,1,2\right\}$$
15	14	imaeq2d	$$⊢\phi \to ⟨“IJK”⟩\left[\mathrm{dom}⟨“IJK”⟩\right]=⟨“IJK”⟩\left[\left\{0,1,2\right\}\right]$$
16		c0ex	$$⊢0\in \mathrm{V}$$
17	16	tpid1	$$⊢0\in \left\{0,1,2\right\}$$
18	17	a1i	$$⊢\phi \to 0\in \left\{0,1,2\right\}$$
19		1ex	$$⊢1\in \mathrm{V}$$
20	19	tpid2	$$⊢1\in \left\{0,1,2\right\}$$
21	20	a1i	$$⊢\phi \to 1\in \left\{0,1,2\right\}$$
22		2ex	$$⊢2\in \mathrm{V}$$
23	22	tpid3	$$⊢2\in \left\{0,1,2\right\}$$
24	23	a1i	$$⊢\phi \to 2\in \left\{0,1,2\right\}$$
25	13 18 21 24	fnimatp	$$⊢\phi \to ⟨“IJK”⟩\left[\left\{0,1,2\right\}\right]=\left\{⟨“IJK”⟩\left(0\right),⟨“IJK”⟩\left(1\right),⟨“IJK”⟩\left(2\right)\right\}$$
26		s3fv0	$$⊢I\in D\to ⟨“IJK”⟩\left(0\right)=I$$
27	1 26	syl	$$⊢\phi \to ⟨“IJK”⟩\left(0\right)=I$$
28		s3fv1	$$⊢J\in D\to ⟨“IJK”⟩\left(1\right)=J$$
29	2 28	syl	$$⊢\phi \to ⟨“IJK”⟩\left(1\right)=J$$
30		s3fv2	$$⊢K\in D\to ⟨“IJK”⟩\left(2\right)=K$$
31	3 30	syl	$$⊢\phi \to ⟨“IJK”⟩\left(2\right)=K$$
32	27 29 31	tpeq123d	$$⊢\phi \to \left\{⟨“IJK”⟩\left(0\right),⟨“IJK”⟩\left(1\right),⟨“IJK”⟩\left(2\right)\right\}=\left\{I,J,K\right\}$$
33	15 25 32	3eqtrd	$$⊢\phi \to ⟨“IJK”⟩\left[\mathrm{dom}⟨“IJK”⟩\right]=\left\{I,J,K\right\}$$
34	4 33	eqtr3id	$$⊢\phi \to \mathrm{ran}⟨“IJK”⟩=\left\{I,J,K\right\}$$