Theorem ccat2s1p1OLD

Description: Obsolete version of ccat2s1p1 as of 20-Jan-2024. Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ccat2s1p1OLD	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		s1cl	⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
2	1	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
3		s1cl	⊢ ( 𝑌 ∈ 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
4	3	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
5		s1len	⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
6	5	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1 )
7		1nn	⊢ 1 ∈ ℕ
8	6 7	eqeltrdi	⊢ ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ∈ ℕ )
9		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ↔ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ∈ ℕ )
10	8 9	sylibr	⊢ ( 𝑋 ∈ 𝑉 → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
11	10	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) )
12		ccatval1OLD	⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) ) ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑋 ”⟩ ‘ 0 ) )
13	2 4 11 12	syl3anc	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑋 ”⟩ ‘ 0 ) )
14		s1fv	⊢ ( 𝑋 ∈ 𝑉 → ( ⟨“ 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
15	14	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ⟨“ 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
16	13 15	eqtrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )