Theorem s1dm

Description: The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020)

	Ref	Expression
Assertion	s1dm	$$⊢\mathrm{dom}⟨“A”⟩=\left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		s1cli	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}$$
2		wrdf	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“A”⟩:\left(0..^\left|⟨“A”⟩\right|\right)⟶\mathrm{V}$$
3	1 2	ax-mp	$$⊢⟨“A”⟩:\left(0..^\left|⟨“A”⟩\right|\right)⟶\mathrm{V}$$
4		s1len	$$⊢\left|⟨“A”⟩\right|=1$$
5		oveq2	$$⊢\left|⟨“A”⟩\right|=1\to \left(0..^\left|⟨“A”⟩\right|\right)=\left(0..^1\right)$$
6		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
7	5 6	eqtrdi	$$⊢\left|⟨“A”⟩\right|=1\to \left(0..^\left|⟨“A”⟩\right|\right)=\left\{0\right\}$$
8	4 7	ax-mp	$$⊢\left(0..^\left|⟨“A”⟩\right|\right)=\left\{0\right\}$$
9	8	eqcomi	$$⊢\left\{0\right\}=\left(0..^\left|⟨“A”⟩\right|\right)$$
10	9	feq2i	$$⊢⟨“A”⟩:\left\{0\right\}⟶\mathrm{V}\leftrightarrow ⟨“A”⟩:\left(0..^\left|⟨“A”⟩\right|\right)⟶\mathrm{V}$$
11	3 10	mpbir	$$⊢⟨“A”⟩:\left\{0\right\}⟶\mathrm{V}$$
12	11	fdmi	$$⊢\mathrm{dom}⟨“A”⟩=\left\{0\right\}$$