Metamath Proof Explorer

Theorem s2rn

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

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 imadmrn 
 |-  ( <" I J "> " dom <" I J "> ) = ran <" I J ">
4 1 2 s2cld 
 |-  ( ph -> <" I J "> e. Word D )
5 wrdfn 
 |-  ( <" I J "> e. Word D -> <" I J "> Fn ( 0 ..^ ( # ` <" I J "> ) ) )
6 s2len 
 |-  ( # ` <" I J "> ) = 2
7 6 oveq2i 
 |-  ( 0 ..^ ( # ` <" I J "> ) ) = ( 0 ..^ 2 )
8 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
9 7 8 eqtri 
 |-  ( 0 ..^ ( # ` <" I J "> ) ) = { 0 , 1 }
10 9 fneq2i 
 |-  ( <" I J "> Fn ( 0 ..^ ( # ` <" I J "> ) ) <-> <" I J "> Fn { 0 , 1 } )
11 10 biimpi 
 |-  ( <" I J "> Fn ( 0 ..^ ( # ` <" I J "> ) ) -> <" I J "> Fn { 0 , 1 } )
12 4 5 11 3syl 
 |-  ( ph -> <" I J "> Fn { 0 , 1 } )
13 12 fndmd 
 |-  ( ph -> dom <" I J "> = { 0 , 1 } )
14 13 imaeq2d 
 |-  ( ph -> ( <" I J "> " dom <" I J "> ) = ( <" I J "> " { 0 , 1 } ) )
15 c0ex 
 |-  0 e. _V
16 15 prid1 
 |-  0 e. { 0 , 1 }
17 16 a1i 
 |-  ( ph -> 0 e. { 0 , 1 } )
18 1ex 
 |-  1 e. _V
19 18 prid2 
 |-  1 e. { 0 , 1 }
20 19 a1i 
 |-  ( ph -> 1 e. { 0 , 1 } )
21 fnimapr 
 |-  ( ( <" I J "> Fn { 0 , 1 } /\ 0 e. { 0 , 1 } /\ 1 e. { 0 , 1 } ) -> ( <" I J "> " { 0 , 1 } ) = { ( <" I J "> ` 0 ) , ( <" I J "> ` 1 ) } )
22 12 17 20 21 syl3anc 
 |-  ( ph -> ( <" I J "> " { 0 , 1 } ) = { ( <" I J "> ` 0 ) , ( <" I J "> ` 1 ) } )
23 s2fv0 
 |-  ( I e. D -> ( <" I J "> ` 0 ) = I )
24 1 23 syl 
 |-  ( ph -> ( <" I J "> ` 0 ) = I )
25 s2fv1 
 |-  ( J e. D -> ( <" I J "> ` 1 ) = J )
26 2 25 syl 
 |-  ( ph -> ( <" I J "> ` 1 ) = J )
27 24 26 preq12d 
 |-  ( ph -> { ( <" I J "> ` 0 ) , ( <" I J "> ` 1 ) } = { I , J } )
28 14 22 27 3eqtrd 
 |-  ( ph -> ( <" I J "> " dom <" I J "> ) = { I , J } )
29 3 28 eqtr3id 
 |-  ( ph -> ran <" I J "> = { I , J } )