Metamath Proof Explorer

Theorem ccat2s1cl

Description: The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018)

		Ref	Expression
	Assertion	ccat2s1cl	$⊢ (X \in V \land Y \in V) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$

Step	Hyp	Ref	Expression
1		s1cl	$⊢ X \in V \to ⟨“ X ”⟩ \in Word V$
2		ccatws1cl	$⊢ (⟨“ X ”⟩ \in Word V \land Y \in V) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
3	1 2	sylan	$⊢ (X \in V \land Y \in V) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$