Theorem s3rn

Description: Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023) (Proof shortened by AV, 1-Aug-2025)

	Ref	Expression
Hypotheses	s2rn.i	$$⊢\phi \to I\in D$$
	s2rn.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		s2rn.i	$$⊢\phi \to I\in D$$
2		s2rn.j	$$⊢\phi \to J\in D$$
3		s3rn.k	$$⊢\phi \to K\in D$$
4		df-s3	$$⊢⟨“IJK”⟩=⟨“IJ”⟩\mathrm{++}⟨“K”⟩$$
5	4	a1i	$$⊢\phi \to ⟨“IJK”⟩=⟨“IJ”⟩\mathrm{++}⟨“K”⟩$$
6	5	rneqd	$$⊢\phi \to \mathrm{ran}⟨“IJK”⟩=\mathrm{ran}\left(⟨“IJ”⟩\mathrm{++}⟨“K”⟩\right)$$
7		s2cli	$$⊢⟨“IJ”⟩\in \mathrm{Word}\mathrm{V}$$
8		s1cli	$$⊢⟨“K”⟩\in \mathrm{Word}\mathrm{V}$$
9	7 8	pm3.2i	$$⊢\left(⟨“IJ”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“K”⟩\in \mathrm{Word}\mathrm{V}\right)$$
10		ccatrn	$$⊢\left(⟨“IJ”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“K”⟩\in \mathrm{Word}\mathrm{V}\right)\to \mathrm{ran}\left(⟨“IJ”⟩\mathrm{++}⟨“K”⟩\right)=\mathrm{ran}⟨“IJ”⟩\cup \mathrm{ran}⟨“K”⟩$$
11	9 10	mp1i	$$⊢\phi \to \mathrm{ran}\left(⟨“IJ”⟩\mathrm{++}⟨“K”⟩\right)=\mathrm{ran}⟨“IJ”⟩\cup \mathrm{ran}⟨“K”⟩$$
12	1 2	s2rn	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\left\{I,J\right\}$$
13		s1rn	$$⊢K\in D\to \mathrm{ran}⟨“K”⟩=\left\{K\right\}$$
14	3 13	syl	$$⊢\phi \to \mathrm{ran}⟨“K”⟩=\left\{K\right\}$$
15	12 14	uneq12d	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩\cup \mathrm{ran}⟨“K”⟩=\left\{I,J\right\}\cup \left\{K\right\}$$
16		df-tp	$$⊢\left\{I,J,K\right\}=\left\{I,J\right\}\cup \left\{K\right\}$$
17	15 16	eqtr4di	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩\cup \mathrm{ran}⟨“K”⟩=\left\{I,J,K\right\}$$
18	6 11 17	3eqtrd	$$⊢\phi \to \mathrm{ran}⟨“IJK”⟩=\left\{I,J,K\right\}$$