This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsws1

Description: The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018)

		Ref	Expression
	Assertion	lsws1	$⊢ A \in V \to lastS (⟨“ A ”⟩) = A$

Step	Hyp	Ref	Expression
1		s1cl	$⊢ A \in V \to ⟨“ A ”⟩ \in Word V$
2		s1len	$⊢ \|⟨“ A ”⟩\| = 1$
3		lsw1	$⊢ (⟨“ A ”⟩ \in Word V \land \|⟨“ A ”⟩\| = 1) \to lastS (⟨“ A ”⟩) = ⟨“ A ”⟩ (0)$
4	1 2 3	sylancl	$⊢ A \in V \to lastS (⟨“ A ”⟩) = ⟨“ A ”⟩ (0)$
5		s1fv	$⊢ A \in V \to ⟨“ A ”⟩ (0) = A$
6	4 5	eqtrd	$⊢ A \in V \to lastS (⟨“ A ”⟩) = A$