Theorem s2rn

Description: Range of a length 2 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$$
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		df-s2	$$⊢⟨“IJ”⟩=⟨“I”⟩\mathrm{++}⟨“J”⟩$$
4	3	a1i	$$⊢\phi \to ⟨“IJ”⟩=⟨“I”⟩\mathrm{++}⟨“J”⟩$$
5	4	rneqd	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\mathrm{ran}\left(⟨“I”⟩\mathrm{++}⟨“J”⟩\right)$$
6		s1cli	$$⊢⟨“I”⟩\in \mathrm{Word}\mathrm{V}$$
7		s1cli	$$⊢⟨“J”⟩\in \mathrm{Word}\mathrm{V}$$
8	6 7	pm3.2i	$$⊢\left(⟨“I”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“J”⟩\in \mathrm{Word}\mathrm{V}\right)$$
9		ccatrn	$$⊢\left(⟨“I”⟩\in \mathrm{Word}\mathrm{V}\wedge ⟨“J”⟩\in \mathrm{Word}\mathrm{V}\right)\to \mathrm{ran}\left(⟨“I”⟩\mathrm{++}⟨“J”⟩\right)=\mathrm{ran}⟨“I”⟩\cup \mathrm{ran}⟨“J”⟩$$
10	8 9	mp1i	$$⊢\phi \to \mathrm{ran}\left(⟨“I”⟩\mathrm{++}⟨“J”⟩\right)=\mathrm{ran}⟨“I”⟩\cup \mathrm{ran}⟨“J”⟩$$
11		s1rn	$$⊢I\in D\to \mathrm{ran}⟨“I”⟩=\left\{I\right\}$$
12	1 11	syl	$$⊢\phi \to \mathrm{ran}⟨“I”⟩=\left\{I\right\}$$
13		s1rn	$$⊢J\in D\to \mathrm{ran}⟨“J”⟩=\left\{J\right\}$$
14	2 13	syl	$$⊢\phi \to \mathrm{ran}⟨“J”⟩=\left\{J\right\}$$
15	12 14	uneq12d	$$⊢\phi \to \mathrm{ran}⟨“I”⟩\cup \mathrm{ran}⟨“J”⟩=\left\{I\right\}\cup \left\{J\right\}$$
16		df-pr	$$⊢\left\{I,J\right\}=\left\{I\right\}\cup \left\{J\right\}$$
17	15 16	eqtr4di	$$⊢\phi \to \mathrm{ran}⟨“I”⟩\cup \mathrm{ran}⟨“J”⟩=\left\{I,J\right\}$$
18	5 10 17	3eqtrd	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\left\{I,J\right\}$$