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

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 ( 𝑋 ∈ 𝑉 → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
2 s1cli ⊢ ⟨“ 𝑌 ”⟩ ∈ Word V
3 s1len ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
4 1nn ⊢ 1 ∈ ℕ
5 3 4 eqeltri ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ∈ ℕ
6 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ↔ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ∈ ℕ )
7 5 6 mpbir ⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) )
8 ccatval1 ⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word V ∧ ⟨“ 𝑌 ”⟩ ∈ Word V ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑋 ”⟩ ‘ 0 ) )
9 1 2 7 8 mp3an ⊢ ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑋 ”⟩ ‘ 0 )
10 s1fv ⊢ ( 𝑋 ∈ 𝑉 → ( ⟨“ 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
11 9 10 eqtrid ⊢ ( 𝑋 ∈ 𝑉 → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )