wrdl1exs1

Description: A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021)

		Ref	Expression
	Assertion	wrdl1exs1	$⊢ (W \in Word S \land \|W\| = 1) \to \exists s \in S W = ⟨“ s ”⟩$

Step	Hyp	Ref	Expression
1		1le1	$⊢ 1 \leq 1$
2		breq2	$⊢ \|W\| = 1 \to (1 \leq \|W\| \leftrightarrow 1 \leq 1)$
3	1 2	mpbiri	$⊢ \|W\| = 1 \to 1 \leq \|W\|$
4		wrdsymb1	$⊢ (W \in Word S \land 1 \leq \|W\|) \to W (0) \in S$
5	3 4	sylan2	$⊢ (W \in Word S \land \|W\| = 1) \to W (0) \in S$
6		s1eq	$⊢ s = W (0) \to ⟨“ s ”⟩ = ⟨“ W (0) ”⟩$
7	6	adantl	$⊢ ((W \in Word S \land \|W\| = 1) \land s = W (0)) \to ⟨“ s ”⟩ = ⟨“ W (0) ”⟩$
8	7	eqeq2d	$⊢ ((W \in Word S \land \|W\| = 1) \land s = W (0)) \to (W = ⟨“ s ”⟩ \leftrightarrow W = ⟨“ W (0) ”⟩)$
9		eqs1	$⊢ (W \in Word S \land \|W\| = 1) \to W = ⟨“ W (0) ”⟩$
10	5 8 9	rspcedvd	$⊢ (W \in Word S \land \|W\| = 1) \to \exists s \in S W = ⟨“ s ”⟩$

Metamath Proof Explorer