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