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 } )