Metamath Proof Explorer

Theorem ccat2s1p1

Description: Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 20-Jan-2024)

Ref Expression
Assertion ccat2s1p1 ⊢ X ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = X

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
2 s1cli ⊢ ⟨“ Y ”⟩ ∈ Word V
3 s1len ⊢ ⟨“ X ”⟩ = 1
4 1nn ⊢ 1 ∈ ℕ
5 3 4 eqeltri ⊢ ⟨“ X ”⟩ ∈ ℕ
6 lbfzo0 ⊢ 0 ∈ 0 ..^ ⟨“ X ”⟩ ↔ ⟨“ X ”⟩ ∈ ℕ
7 5 6 mpbir ⊢ 0 ∈ 0 ..^ ⟨“ X ”⟩
8 ccatval1 ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V ∧ 0 ∈ 0 ..^ ⟨“ X ”⟩ → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = ⟨“ X ”⟩ ⁡ 0
9 1 2 7 8 mp3an ⊢ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = ⟨“ X ”⟩ ⁡ 0
10 s1fv ⊢ X ∈ V → ⟨“ X ”⟩ ⁡ 0 = X
11 9 10 syl5eq ⊢ X ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = X