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 
|- ( ph -> I e. D )
s2rn.j 
|- ( ph -> J e. D )
Assertion s2rn 
|- ( ph -> ran <" I J "> = { I , J } )

Proof

Step Hyp Ref Expression
1 s2rn.i 
 |-  ( ph -> I e. D )
2 s2rn.j 
 |-  ( ph -> J e. D )
3 df-s2 
 |-  <" I J "> = ( <" I "> ++ <" J "> )
4 3 a1i 
 |-  ( ph -> <" I J "> = ( <" I "> ++ <" J "> ) )
5 4 rneqd 
 |-  ( ph -> ran <" I J "> = ran ( <" I "> ++ <" J "> ) )
6 s1cli 
 |-  <" I "> e. Word _V
7 s1cli 
 |-  <" J "> e. Word _V
8 6 7 pm3.2i 
 |-  ( <" I "> e. Word _V /\ <" J "> e. Word _V )
9 ccatrn 
 |-  ( ( <" I "> e. Word _V /\ <" J "> e. Word _V ) -> ran ( <" I "> ++ <" J "> ) = ( ran <" I "> u. ran <" J "> ) )
10 8 9 mp1i 
 |-  ( ph -> ran ( <" I "> ++ <" J "> ) = ( ran <" I "> u. ran <" J "> ) )
11 s1rn 
 |-  ( I e. D -> ran <" I "> = { I } )
12 1 11 syl 
 |-  ( ph -> ran <" I "> = { I } )
13 s1rn 
 |-  ( J e. D -> ran <" J "> = { J } )
14 2 13 syl 
 |-  ( ph -> ran <" J "> = { J } )
15 12 14 uneq12d 
 |-  ( ph -> ( ran <" I "> u. ran <" J "> ) = ( { I } u. { J } ) )
16 df-pr 
 |-  { I , J } = ( { I } u. { J } )
17 15 16 eqtr4di 
 |-  ( ph -> ( ran <" I "> u. ran <" J "> ) = { I , J } )
18 5 10 17 3eqtrd 
 |-  ( ph -> ran <" I J "> = { I , J } )