ccats1alpha

Description: A concatenation of a word with a singleton word is a word over an alphabet S iff the symbols of both words belong to the alphabet S . (Contributed by AV, 27-Mar-2022)

		Ref	Expression
	Assertion	ccats1alpha	$⊢ (A \in Word V \land X \in U) \to (A ++ ⟨“ X ”⟩ \in Word S \leftrightarrow (A \in Word S \land X \in S))$

Proof

Step	Hyp	Ref	Expression
1		wrdv	$⊢ A \in Word V \to A \in Word V$
2		s1cli	$⊢ ⟨“ X ”⟩ \in Word V$
3	2	a1i	$⊢ X \in U \to ⟨“ X ”⟩ \in Word V$
4		ccatalpha	$⊢ (A \in Word V \land ⟨“ X ”⟩ \in Word V) \to (A ++ ⟨“ X ”⟩ \in Word S \leftrightarrow (A \in Word S \land ⟨“ X ”⟩ \in Word S))$
5	1 3 4	syl2an	$⊢ (A \in Word V \land X \in U) \to (A ++ ⟨“ X ”⟩ \in Word S \leftrightarrow (A \in Word S \land ⟨“ X ”⟩ \in Word S))$
6		simpr	$⊢ (X \in U \land ⟨“ X ”⟩ \in Word S) \to ⟨“ X ”⟩ \in Word S$
7		s1len	$⊢ \|⟨“ X ”⟩\| = 1$
8		wrdl1exs1	$⊢ (⟨“ X ”⟩ \in Word S \land \|⟨“ X ”⟩\| = 1) \to \exists w \in S ⟨“ X ”⟩ = ⟨“ w ”⟩$
9	6 7 8	sylancl	$⊢ (X \in U \land ⟨“ X ”⟩ \in Word S) \to \exists w \in S ⟨“ X ”⟩ = ⟨“ w ”⟩$
10		elex	$⊢ X \in U \to X \in V$
11	10	adantr	$⊢ (X \in U \land ⟨“ X ”⟩ \in Word S) \to X \in V$
12		elex	$⊢ w \in S \to w \in V$
13		s111	$⊢ (X \in V \land w \in V) \to (⟨“ X ”⟩ = ⟨“ w ”⟩ \leftrightarrow X = w)$
14	11 12 13	syl2an	$⊢ ((X \in U \land ⟨“ X ”⟩ \in Word S) \land w \in S) \to (⟨“ X ”⟩ = ⟨“ w ”⟩ \leftrightarrow X = w)$
15		simpr	$⊢ ((X \in U \land ⟨“ X ”⟩ \in Word S) \land w \in S) \to w \in S$
16		eleq1	$⊢ X = w \to (X \in S \leftrightarrow w \in S)$
17	15 16	syl5ibrcom	$⊢ ((X \in U \land ⟨“ X ”⟩ \in Word S) \land w \in S) \to (X = w \to X \in S)$
18	14 17	sylbid	$⊢ ((X \in U \land ⟨“ X ”⟩ \in Word S) \land w \in S) \to (⟨“ X ”⟩ = ⟨“ w ”⟩ \to X \in S)$
19	18	rexlimdva	$⊢ (X \in U \land ⟨“ X ”⟩ \in Word S) \to (\exists w \in S ⟨“ X ”⟩ = ⟨“ w ”⟩ \to X \in S)$
20	9 19	mpd	$⊢ (X \in U \land ⟨“ X ”⟩ \in Word S) \to X \in S$
21	20	ex	$⊢ X \in U \to (⟨“ X ”⟩ \in Word S \to X \in S)$
22		s1cl	$⊢ X \in S \to ⟨“ X ”⟩ \in Word S$
23	21 22	impbid1	$⊢ X \in U \to (⟨“ X ”⟩ \in Word S \leftrightarrow X \in S)$
24	23	anbi2d	$⊢ X \in U \to ((A \in Word S \land ⟨“ X ”⟩ \in Word S) \leftrightarrow (A \in Word S \land X \in S))$
25	24	adantl	$⊢ (A \in Word V \land X \in U) \to ((A \in Word S \land ⟨“ X ”⟩ \in Word S) \leftrightarrow (A \in Word S \land X \in S))$
26	5 25	bitrd	$⊢ (A \in Word V \land X \in U) \to (A ++ ⟨“ X ”⟩ \in Word S \leftrightarrow (A \in Word S \land X \in S))$

Metamath Proof Explorer

Theorem ccats1alpha

Proof