Metamath Proof Explorer

Theorem wrdl1s1

Description: A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	wrdl1s1	$⊢ S \in V \to (W = ⟨“ S ”⟩ \leftrightarrow (W \in Word V \land \|W\| = 1 \land W (0) = S))$

Proof

Step	Hyp	Ref	Expression
1		s1cl	$⊢ S \in V \to ⟨“ S ”⟩ \in Word V$
2		s1len	$⊢ \|⟨“ S ”⟩\| = 1$
3	2	a1i	$⊢ S \in V \to \|⟨“ S ”⟩\| = 1$
4		s1fv	$⊢ S \in V \to ⟨“ S ”⟩ (0) = S$
5	1 3 4	3jca	$⊢ S \in V \to (⟨“ S ”⟩ \in Word V \land \|⟨“ S ”⟩\| = 1 \land ⟨“ S ”⟩ (0) = S)$
6		eleq1	$⊢ W = ⟨“ S ”⟩ \to (W \in Word V \leftrightarrow ⟨“ S ”⟩ \in Word V)$
7		fveqeq2	$⊢ W = ⟨“ S ”⟩ \to (\|W\| = 1 \leftrightarrow \|⟨“ S ”⟩\| = 1)$
8		fveq1	$⊢ W = ⟨“ S ”⟩ \to W (0) = ⟨“ S ”⟩ (0)$
9	8	eqeq1d	$⊢ W = ⟨“ S ”⟩ \to (W (0) = S \leftrightarrow ⟨“ S ”⟩ (0) = S)$
10	6 7 9	3anbi123d	$⊢ W = ⟨“ S ”⟩ \to ((W \in Word V \land \|W\| = 1 \land W (0) = S) \leftrightarrow (⟨“ S ”⟩ \in Word V \land \|⟨“ S ”⟩\| = 1 \land ⟨“ S ”⟩ (0) = S))$
11	5 10	syl5ibrcom	$⊢ S \in V \to (W = ⟨“ S ”⟩ \to (W \in Word V \land \|W\| = 1 \land W (0) = S))$
12		eqs1	$⊢ (W \in Word V \land \|W\| = 1) \to W = ⟨“ W (0) ”⟩$
13		s1eq	$⊢ W (0) = S \to ⟨“ W (0) ”⟩ = ⟨“ S ”⟩$
14	13	eqeq2d	$⊢ W (0) = S \to (W = ⟨“ W (0) ”⟩ \leftrightarrow W = ⟨“ S ”⟩)$
15	12 14	syl5ibcom	$⊢ (W \in Word V \land \|W\| = 1) \to (W (0) = S \to W = ⟨“ S ”⟩)$
16	15	3impia	$⊢ (W \in Word V \land \|W\| = 1 \land W (0) = S) \to W = ⟨“ S ”⟩$
17	11 16	impbid1	$⊢ S \in V \to (W = ⟨“ S ”⟩ \leftrightarrow (W \in Word V \land \|W\| = 1 \land W (0) = S))$