Metamath Proof Explorer

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 ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = X

Proof

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