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

Proof

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