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

Metamath Proof Explorer

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