Theorem s1len

Description: Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s1len	$$⊢\left|⟨“A”⟩\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		df-s1	$$⊢⟨“A”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
2	1	fveq2i	$$⊢\left|⟨“A”⟩\right|=\left|\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}\right|$$
3		opex	$$⊢⟨0,\mathrm{I}\left(A\right)⟩\in \mathrm{V}$$
4		hashsng	$$⊢⟨0,\mathrm{I}\left(A\right)⟩\in \mathrm{V}\to \left|\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}\right|=1$$
5	3 4	ax-mp	$$⊢\left|\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}\right|=1$$
6	2 5	eqtri	$$⊢\left|⟨“A”⟩\right|=1$$