This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⟨“ 𝐼 𝐽 𝐾 ”⟩ = { 𝐼 , 𝐽 , 𝐾 } )