Metamath Proof Explorer


Theorem s2rn

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

Ref Expression
Hypotheses s2rn.i φ I D
s2rn.j φ J D
Assertion s2rn φ ran ⟨“ IJ ”⟩ = I J

Proof

Step Hyp Ref Expression
1 s2rn.i φ I D
2 s2rn.j φ J D
3 imadmrn ⟨“ IJ ”⟩ dom ⟨“ IJ ”⟩ = ran ⟨“ IJ ”⟩
4 1 2 s2cld φ ⟨“ IJ ”⟩ Word D
5 wrdfn ⟨“ IJ ”⟩ Word D ⟨“ IJ ”⟩ Fn 0 ..^ ⟨“ IJ ”⟩
6 s2len ⟨“ IJ ”⟩ = 2
7 6 oveq2i 0 ..^ ⟨“ IJ ”⟩ = 0 ..^ 2
8 fzo0to2pr 0 ..^ 2 = 0 1
9 7 8 eqtri 0 ..^ ⟨“ IJ ”⟩ = 0 1
10 9 fneq2i ⟨“ IJ ”⟩ Fn 0 ..^ ⟨“ IJ ”⟩ ⟨“ IJ ”⟩ Fn 0 1
11 10 biimpi ⟨“ IJ ”⟩ Fn 0 ..^ ⟨“ IJ ”⟩ ⟨“ IJ ”⟩ Fn 0 1
12 4 5 11 3syl φ ⟨“ IJ ”⟩ Fn 0 1
13 12 fndmd φ dom ⟨“ IJ ”⟩ = 0 1
14 13 imaeq2d φ ⟨“ IJ ”⟩ dom ⟨“ IJ ”⟩ = ⟨“ IJ ”⟩ 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 ⟨“ IJ ”⟩ Fn 0 1 0 0 1 1 0 1 ⟨“ IJ ”⟩ 0 1 = ⟨“ IJ ”⟩ 0 ⟨“ IJ ”⟩ 1
22 12 17 20 21 syl3anc φ ⟨“ IJ ”⟩ 0 1 = ⟨“ IJ ”⟩ 0 ⟨“ IJ ”⟩ 1
23 s2fv0 I D ⟨“ IJ ”⟩ 0 = I
24 1 23 syl φ ⟨“ IJ ”⟩ 0 = I
25 s2fv1 J D ⟨“ IJ ”⟩ 1 = J
26 2 25 syl φ ⟨“ IJ ”⟩ 1 = J
27 24 26 preq12d φ ⟨“ IJ ”⟩ 0 ⟨“ IJ ”⟩ 1 = I J
28 14 22 27 3eqtrd φ ⟨“ IJ ”⟩ dom ⟨“ IJ ”⟩ = I J
29 3 28 eqtr3id φ ran ⟨“ IJ ”⟩ = I J