Metamath Proof Explorer

Theorem ccats1pfxeqrex

Description: There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion ccats1pfxeqrex ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W → ∃ s ∈ V U = W ++ ⟨“ s ”⟩

Proof

Step Hyp Ref Expression
1 simp2 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U ∈ Word V
2 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
3 2 3ad2ant1 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W ∈ ℕ 0
4 nn0p1nn ⊢ W ∈ ℕ 0 → W + 1 ∈ ℕ
5 nngt0 ⊢ W + 1 ∈ ℕ → 0 < W + 1
6 3 4 5 3syl ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < W + 1
7 breq2 ⊢ U = W + 1 → 0 < U ↔ 0 < W + 1
8 7 3ad2ant3 ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < U ↔ 0 < W + 1
9 6 8 mpbird ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → 0 < U
10 hashgt0n0 ⊢ U ∈ Word V ∧ 0 < U → U ≠ ∅
11 1 9 10 syl2anc ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → U ≠ ∅
12 lswcl ⊢ U ∈ Word V ∧ U ≠ ∅ → lastS ⁡ U ∈ V
13 1 11 12 syl2anc ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → lastS ⁡ U ∈ V
14 ccats1pfxeq ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W → U = W ++ ⟨“ lastS ⁡ U ”⟩
15 s1eq ⊢ s = lastS ⁡ U → ⟨“ s ”⟩ = ⟨“ lastS ⁡ U ”⟩
16 15 oveq2d ⊢ s = lastS ⁡ U → W ++ ⟨“ s ”⟩ = W ++ ⟨“ lastS ⁡ U ”⟩
17 16 rspceeqv ⊢ lastS ⁡ U ∈ V ∧ U = W ++ ⟨“ lastS ⁡ U ”⟩ → ∃ s ∈ V U = W ++ ⟨“ s ”⟩
18 13 14 17 syl6an ⊢ W ∈ Word V ∧ U ∈ Word V ∧ U = W + 1 → W = U prefix W → ∃ s ∈ V U = W ++ ⟨“ s ”⟩