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

Proof

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