Metamath Proof Explorer


Theorem s2rn

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

Ref Expression
Hypotheses s2rn.i ( 𝜑𝐼𝐷 )
s2rn.j ( 𝜑𝐽𝐷 )
Assertion s2rn ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )

Proof

Step Hyp Ref Expression
1 s2rn.i ( 𝜑𝐼𝐷 )
2 s2rn.j ( 𝜑𝐽𝐷 )
3 imadmrn ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = ran ⟨“ 𝐼 𝐽 ”⟩
4 1 2 s2cld ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
5 wrdfn ( ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 → ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) )
6 s2len ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = 2
7 6 oveq2i ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 0 ..^ 2 )
8 fzo0to2pr ( 0 ..^ 2 ) = { 0 , 1 }
9 7 8 eqtri ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = { 0 , 1 }
10 9 fneq2i ( ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) ↔ ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
11 10 biimpi ( ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) → ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
12 4 5 11 3syl ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
13 12 fndmd ( 𝜑 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
14 13 imaeq2d ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) )
15 c0ex 0 ∈ V
16 15 prid1 0 ∈ { 0 , 1 }
17 16 a1i ( 𝜑 → 0 ∈ { 0 , 1 } )
18 1ex 1 ∈ V
19 18 prid2 1 ∈ { 0 , 1 }
20 19 a1i ( 𝜑 → 1 ∈ { 0 , 1 } )
21 fnimapr ( ( ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } ∧ 0 ∈ { 0 , 1 } ∧ 1 ∈ { 0 , 1 } ) → ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) = { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } )
22 12 17 20 21 syl3anc ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) = { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } )
23 s2fv0 ( 𝐼𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
24 1 23 syl ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
25 s2fv1 ( 𝐽𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
26 2 25 syl ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
27 24 26 preq12d ( 𝜑 → { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } = { 𝐼 , 𝐽 } )
28 14 22 27 3eqtrd ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = { 𝐼 , 𝐽 } )
29 3 28 eqtr3id ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )