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	|- ( ph -> S e. V )
	s1mapd.x	|- ( ph -> X e. S )
Assertion	s1mapd	|- ( ph -> <" X "> e. ( S ^m { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		s1mapd.1	|- ( ph -> S e. V )
2		s1mapd.x	|- ( ph -> X e. S )
3		ovexd	|- ( ph -> ( 0 ..^ 1 ) e. _V )
4		s1len	|- ( # ` <" X "> ) = 1
5	4	a1i	|- ( ph -> ( # ` <" X "> ) = 1 )
6	5	eqcomd	|- ( ph -> 1 = ( # ` <" X "> ) )
7	2	s1cld	|- ( ph -> <" X "> e. Word S )
8	6 7	wrdfd	|- ( ph -> <" X "> : ( 0 ..^ 1 ) --> S )
9	1 3 8	elmapdd	|- ( ph -> <" X "> e. ( S ^m ( 0 ..^ 1 ) ) )
10		fzo01	|- ( 0 ..^ 1 ) = { 0 }
11	10	oveq2i	|- ( S ^m ( 0 ..^ 1 ) ) = ( S ^m { 0 } )
12	9 11	eleqtrdi	|- ( ph -> <" X "> e. ( S ^m { 0 } ) )