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