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	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	s2rn.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
Assertion	s2rn	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )

Proof

Step	Hyp	Ref	Expression
1		s2rn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2		s2rn.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
3		df-s2	⊢ ⟨“ 𝐼 𝐽 ”⟩ = ( ⟨“ 𝐼 ”⟩ ++ ⟨“ 𝐽 ”⟩ )
4	3	a1i	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ = ( ⟨“ 𝐼 ”⟩ ++ ⟨“ 𝐽 ”⟩ ) )
5	4	rneqd	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = ran ( ⟨“ 𝐼 ”⟩ ++ ⟨“ 𝐽 ”⟩ ) )
6		s1cli	⊢ ⟨“ 𝐼 ”⟩ ∈ Word V
7		s1cli	⊢ ⟨“ 𝐽 ”⟩ ∈ Word V
8	6 7	pm3.2i	⊢ ( ⟨“ 𝐼 ”⟩ ∈ Word V ∧ ⟨“ 𝐽 ”⟩ ∈ Word V )
9		ccatrn	⊢ ( ( ⟨“ 𝐼 ”⟩ ∈ Word V ∧ ⟨“ 𝐽 ”⟩ ∈ Word V ) → ran ( ⟨“ 𝐼 ”⟩ ++ ⟨“ 𝐽 ”⟩ ) = ( ran ⟨“ 𝐼 ”⟩ ∪ ran ⟨“ 𝐽 ”⟩ ) )
10	8 9	mp1i	⊢ ( 𝜑 → ran ( ⟨“ 𝐼 ”⟩ ++ ⟨“ 𝐽 ”⟩ ) = ( ran ⟨“ 𝐼 ”⟩ ∪ ran ⟨“ 𝐽 ”⟩ ) )
11		s1rn	⊢ ( 𝐼 ∈ 𝐷 → ran ⟨“ 𝐼 ”⟩ = { 𝐼 } )
12	1 11	syl	⊢ ( 𝜑 → ran ⟨“ 𝐼 ”⟩ = { 𝐼 } )
13		s1rn	⊢ ( 𝐽 ∈ 𝐷 → ran ⟨“ 𝐽 ”⟩ = { 𝐽 } )
14	2 13	syl	⊢ ( 𝜑 → ran ⟨“ 𝐽 ”⟩ = { 𝐽 } )
15	12 14	uneq12d	⊢ ( 𝜑 → ( ran ⟨“ 𝐼 ”⟩ ∪ ran ⟨“ 𝐽 ”⟩ ) = ( { 𝐼 } ∪ { 𝐽 } ) )
16		df-pr	⊢ { 𝐼 , 𝐽 } = ( { 𝐼 } ∪ { 𝐽 } )
17	15 16	eqtr4di	⊢ ( 𝜑 → ( ran ⟨“ 𝐼 ”⟩ ∪ ran ⟨“ 𝐽 ”⟩ ) = { 𝐼 , 𝐽 } )
18	5 10 17	3eqtrd	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )