Metamath Proof Explorer


Theorem s3rn

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

Ref Expression
Hypotheses s3rn.i φ I D
s3rn.j φ J D
s3rn.k φ K D
Assertion s3rn φ ran ⟨“ IJK ”⟩ = I J K

Proof

Step Hyp Ref Expression
1 s3rn.i φ I D
2 s3rn.j φ J D
3 s3rn.k φ K D
4 imadmrn ⟨“ IJK ”⟩ dom ⟨“ IJK ”⟩ = ran ⟨“ IJK ”⟩
5 1 2 3 s3cld φ ⟨“ IJK ”⟩ Word D
6 wrdfn ⟨“ IJK ”⟩ Word D ⟨“ IJK ”⟩ Fn 0 ..^ ⟨“ IJK ”⟩
7 s3len ⟨“ IJK ”⟩ = 3
8 7 oveq2i 0 ..^ ⟨“ IJK ”⟩ = 0 ..^ 3
9 fzo0to3tp 0 ..^ 3 = 0 1 2
10 8 9 eqtri 0 ..^ ⟨“ IJK ”⟩ = 0 1 2
11 10 fneq2i ⟨“ IJK ”⟩ Fn 0 ..^ ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ Fn 0 1 2
12 11 biimpi ⟨“ IJK ”⟩ Fn 0 ..^ ⟨“ IJK ”⟩ ⟨“ IJK ”⟩ Fn 0 1 2
13 5 6 12 3syl φ ⟨“ IJK ”⟩ Fn 0 1 2
14 13 fndmd φ dom ⟨“ IJK ”⟩ = 0 1 2
15 14 imaeq2d φ ⟨“ IJK ”⟩ dom ⟨“ IJK ”⟩ = ⟨“ IJK ”⟩ 0 1 2
16 c0ex 0 V
17 16 tpid1 0 0 1 2
18 17 a1i φ 0 0 1 2
19 1ex 1 V
20 19 tpid2 1 0 1 2
21 20 a1i φ 1 0 1 2
22 2ex 2 V
23 22 tpid3 2 0 1 2
24 23 a1i φ 2 0 1 2
25 13 18 21 24 fnimatp φ ⟨“ IJK ”⟩ 0 1 2 = ⟨“ IJK ”⟩ 0 ⟨“ IJK ”⟩ 1 ⟨“ IJK ”⟩ 2
26 s3fv0 I D ⟨“ IJK ”⟩ 0 = I
27 1 26 syl φ ⟨“ IJK ”⟩ 0 = I
28 s3fv1 J D ⟨“ IJK ”⟩ 1 = J
29 2 28 syl φ ⟨“ IJK ”⟩ 1 = J
30 s3fv2 K D ⟨“ IJK ”⟩ 2 = K
31 3 30 syl φ ⟨“ IJK ”⟩ 2 = K
32 27 29 31 tpeq123d φ ⟨“ IJK ”⟩ 0 ⟨“ IJK ”⟩ 1 ⟨“ IJK ”⟩ 2 = I J K
33 15 25 32 3eqtrd φ ⟨“ IJK ”⟩ dom ⟨“ IJK ”⟩ = I J K
34 4 33 eqtr3id φ ran ⟨“ IJK ”⟩ = I J K