This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cats1fv

Description: A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
cats1cli.2 ⊢ S ∈ Word V
cats1fvn.3 ⊢ S = M
cats1fv.4 ⊢ Y ∈ V → S ⁡ N = Y
cats1fv.5 ⊢ N ∈ ℕ 0
cats1fv.6 ⊢ N < M
Assertion cats1fv ⊢ Y ∈ V → T ⁡ N = Y

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cli.2 ⊢ S ∈ Word V
3 cats1fvn.3 ⊢ S = M
4 cats1fv.4 ⊢ Y ∈ V → S ⁡ N = Y
5 cats1fv.5 ⊢ N ∈ ℕ 0
6 cats1fv.6 ⊢ N < M
7 1 fveq1i ⊢ T ⁡ N = S ++ ⟨“ X ”⟩ ⁡ N
8 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
9 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
10 5 9 eleqtri ⊢ N ∈ ℤ ≥ 0
11 lencl ⊢ S ∈ Word V → S ∈ ℕ 0
12 nn0z ⊢ S ∈ ℕ 0 → S ∈ ℤ
13 2 11 12 mp2b ⊢ S ∈ ℤ
14 6 3 breqtrri ⊢ N < S
15 elfzo2 ⊢ N ∈ 0 ..^ S ↔ N ∈ ℤ ≥ 0 ∧ S ∈ ℤ ∧ N < S
16 10 13 14 15 mpbir3an ⊢ N ∈ 0 ..^ S
17 ccatval1 ⊢ S ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V ∧ N ∈ 0 ..^ S → S ++ ⟨“ X ”⟩ ⁡ N = S ⁡ N
18 2 8 16 17 mp3an ⊢ S ++ ⟨“ X ”⟩ ⁡ N = S ⁡ N
19 7 18 eqtri ⊢ T ⁡ N = S ⁡ N
20 19 4 eqtrid ⊢ Y ∈ V → T ⁡ N = Y