Metamath Proof Explorer

Theorem s3rn

Description: Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s3rn.i 
|- ( ph -> I e. D )
s3rn.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 s3rn.i 
 |-  ( ph -> I e. D )
2 s3rn.j 
 |-  ( ph -> J e. D )
3 s3rn.k 
 |-  ( ph -> K e. D )
4 imadmrn 
 |-  ( <" I J K "> " dom <" I J K "> ) = ran <" I J K ">
5 1 2 3 s3cld 
 |-  ( ph -> <" I J K "> e. Word D )
6 wrdfn 
 |-  ( <" I J K "> e. Word D -> <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) )
7 s3len 
 |-  ( # ` <" I J K "> ) = 3
8 7 oveq2i 
 |-  ( 0 ..^ ( # ` <" I J K "> ) ) = ( 0 ..^ 3 )
9 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 8 9 eqtri 
 |-  ( 0 ..^ ( # ` <" I J K "> ) ) = { 0 , 1 , 2 }
11 10 fneq2i 
 |-  ( <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) <-> <" I J K "> Fn { 0 , 1 , 2 } )
12 11 biimpi 
 |-  ( <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) -> <" I J K "> Fn { 0 , 1 , 2 } )
13 5 6 12 3syl 
 |-  ( ph -> <" I J K "> Fn { 0 , 1 , 2 } )
14 13 fndmd 
 |-  ( ph -> dom <" I J K "> = { 0 , 1 , 2 } )
15 14 imaeq2d 
 |-  ( ph -> ( <" I J K "> " dom <" I J K "> ) = ( <" I J K "> " { 0 , 1 , 2 } ) )
16 c0ex 
 |-  0 e. _V
17 16 tpid1 
 |-  0 e. { 0 , 1 , 2 }
18 17 a1i 
 |-  ( ph -> 0 e. { 0 , 1 , 2 } )
19 1ex 
 |-  1 e. _V
20 19 tpid2 
 |-  1 e. { 0 , 1 , 2 }
21 20 a1i 
 |-  ( ph -> 1 e. { 0 , 1 , 2 } )
22 2ex 
 |-  2 e. _V
23 22 tpid3 
 |-  2 e. { 0 , 1 , 2 }
24 23 a1i 
 |-  ( ph -> 2 e. { 0 , 1 , 2 } )
25 13 18 21 24 fnimatp 
 |-  ( ph -> ( <" I J K "> " { 0 , 1 , 2 } ) = { ( <" I J K "> ` 0 ) , ( <" I J K "> ` 1 ) , ( <" I J K "> ` 2 ) } )
26 s3fv0 
 |-  ( I e. D -> ( <" I J K "> ` 0 ) = I )
27 1 26 syl 
 |-  ( ph -> ( <" I J K "> ` 0 ) = I )
28 s3fv1 
 |-  ( J e. D -> ( <" I J K "> ` 1 ) = J )
29 2 28 syl 
 |-  ( ph -> ( <" I J K "> ` 1 ) = J )
30 s3fv2 
 |-  ( K e. D -> ( <" I J K "> ` 2 ) = K )
31 3 30 syl 
 |-  ( ph -> ( <" I J K "> ` 2 ) = K )
32 27 29 31 tpeq123d 
 |-  ( ph -> { ( <" I J K "> ` 0 ) , ( <" I J K "> ` 1 ) , ( <" I J K "> ` 2 ) } = { I , J , K } )
33 15 25 32 3eqtrd 
 |-  ( ph -> ( <" I J K "> " dom <" I J K "> ) = { I , J , K } )
34 4 33 eqtr3id 
 |-  ( ph -> ran <" I J K "> = { I , J , K } )