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 ) = 𝑋 )