Metamath Proof Explorer

Theorem s3rnOLD

Description: Obsolete version of s2rn as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses s3rnOLD.i ⊢ φ → I ∈ D
s3rnOLD.j ⊢ φ → J ∈ D
s3rnOLD.k ⊢ φ → K ∈ D
Assertion s3rnOLD ⊢ φ → ran ⁡ ⟨“ IJK ”⟩ = I J K

Proof

Step Hyp Ref Expression
1 s3rnOLD.i ⊢ φ → I ∈ D
2 s3rnOLD.j ⊢ φ → J ∈ D
3 s3rnOLD.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 fnimatpd ⊢ φ → ⟨“ 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