Theorem s2rn

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

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

Proof

Step	Hyp	Ref	Expression
1		s2rn.i	$$⊢\phi \to I\in D$$
2		s2rn.j	$$⊢\phi \to J\in D$$
3		imadmrn	$$⊢⟨“IJ”⟩\left[\mathrm{dom}⟨“IJ”⟩\right]=\mathrm{ran}⟨“IJ”⟩$$
4	1 2	s2cld	$$⊢\phi \to ⟨“IJ”⟩\in \mathrm{Word}D$$
5		wrdfn	$$⊢⟨“IJ”⟩\in \mathrm{Word}D\to ⟨“IJ”⟩Fn\left(0..^\left|⟨“IJ”⟩\right|\right)$$
6		s2len	$$⊢\left|⟨“IJ”⟩\right|=2$$
7	6	oveq2i	$$⊢\left(0..^\left|⟨“IJ”⟩\right|\right)=\left(0..^2\right)$$
8		fzo0to2pr	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$
9	7 8	eqtri	$$⊢\left(0..^\left|⟨“IJ”⟩\right|\right)=\left\{0,1\right\}$$
10	9	fneq2i	$$⊢⟨“IJ”⟩Fn\left(0..^\left|⟨“IJ”⟩\right|\right)\leftrightarrow ⟨“IJ”⟩Fn\left\{0,1\right\}$$
11	10	biimpi	$$⊢⟨“IJ”⟩Fn\left(0..^\left|⟨“IJ”⟩\right|\right)\to ⟨“IJ”⟩Fn\left\{0,1\right\}$$
12	4 5 11	3syl	$$⊢\phi \to ⟨“IJ”⟩Fn\left\{0,1\right\}$$
13	12	fndmd	$$⊢\phi \to \mathrm{dom}⟨“IJ”⟩=\left\{0,1\right\}$$
14	13	imaeq2d	$$⊢\phi \to ⟨“IJ”⟩\left[\mathrm{dom}⟨“IJ”⟩\right]=⟨“IJ”⟩\left[\left\{0,1\right\}\right]$$
15		c0ex	$$⊢0\in \mathrm{V}$$
16	15	prid1	$$⊢0\in \left\{0,1\right\}$$
17	16	a1i	$$⊢\phi \to 0\in \left\{0,1\right\}$$
18		1ex	$$⊢1\in \mathrm{V}$$
19	18	prid2	$$⊢1\in \left\{0,1\right\}$$
20	19	a1i	$$⊢\phi \to 1\in \left\{0,1\right\}$$
21		fnimapr	$$⊢\left(⟨“IJ”⟩Fn\left\{0,1\right\}\wedge 0\in \left\{0,1\right\}\wedge 1\in \left\{0,1\right\}\right)\to ⟨“IJ”⟩\left[\left\{0,1\right\}\right]=\left\{⟨“IJ”⟩\left(0\right),⟨“IJ”⟩\left(1\right)\right\}$$
22	12 17 20 21	syl3anc	$$⊢\phi \to ⟨“IJ”⟩\left[\left\{0,1\right\}\right]=\left\{⟨“IJ”⟩\left(0\right),⟨“IJ”⟩\left(1\right)\right\}$$
23		s2fv0	$$⊢I\in D\to ⟨“IJ”⟩\left(0\right)=I$$
24	1 23	syl	$$⊢\phi \to ⟨“IJ”⟩\left(0\right)=I$$
25		s2fv1	$$⊢J\in D\to ⟨“IJ”⟩\left(1\right)=J$$
26	2 25	syl	$$⊢\phi \to ⟨“IJ”⟩\left(1\right)=J$$
27	24 26	preq12d	$$⊢\phi \to \left\{⟨“IJ”⟩\left(0\right),⟨“IJ”⟩\left(1\right)\right\}=\left\{I,J\right\}$$
28	14 22 27	3eqtrd	$$⊢\phi \to ⟨“IJ”⟩\left[\mathrm{dom}⟨“IJ”⟩\right]=\left\{I,J\right\}$$
29	3 28	eqtr3id	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\left\{I,J\right\}$$