Theorem s1mapd

Description: A singleton word is a function on the singleton { 0 } . See also s2mapd . (Contributed by Thierry Arnoux, 10-Oct-2026)

	Ref	Expression
Hypotheses	s1mapd.1	$$⊢\phi \to S\in V$$
	s1mapd.x	$$⊢\phi \to X\in S$$
Assertion	s1mapd	$$⊢\phi \to ⟨“X”⟩\in \left(S^{\left\{0\right\}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		s1mapd.1	$$⊢\phi \to S\in V$$
2		s1mapd.x	$$⊢\phi \to X\in S$$
3		ovexd	$$⊢\phi \to \left(0..^1\right)\in \mathrm{V}$$
4		s1len	$$⊢\left|⟨“X”⟩\right|=1$$
5	4	a1i	$$⊢\phi \to \left|⟨“X”⟩\right|=1$$
6	5	eqcomd	$$⊢\phi \to 1=\left|⟨“X”⟩\right|$$
7	2	s1cld	$$⊢\phi \to ⟨“X”⟩\in \mathrm{Word}S$$
8	6 7	wrdfd	$$⊢\phi \to ⟨“X”⟩:\left(0..^1\right)⟶S$$
9	1 3 8	elmapdd	$$⊢\phi \to ⟨“X”⟩\in \left(S^{\left(0..^1\right)}\right)$$
10		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
11	10	oveq2i	$$⊢S^{\left(0..^1\right)}=S^{\left\{0\right\}}$$
12	9 11	eleqtrdi	$$⊢\phi \to ⟨“X”⟩\in \left(S^{\left\{0\right\}}\right)$$