Theorem s2mapd

Description: A doubleton word is a function on the doubleton ( 0 ..^ 2 ) (which is equal to { 0 , 1 } by fzo0to2pr ). See also s3rexrd . (Contributed by Thierry Arnoux, 10-Oct-2026)

	Ref	Expression
Hypotheses	s2mapd.s	|- ( ph -> S e. V )
	s2mapd.x	|- ( ph -> X e. S )
	s2mapd.y	|- ( ph -> Y e. S )
Assertion	s2mapd	|- ( ph -> <" X Y "> e. ( S ^m ( 0 ..^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s2mapd.s	|- ( ph -> S e. V )
2		s2mapd.x	|- ( ph -> X e. S )
3		s2mapd.y	|- ( ph -> Y e. S )
4		ovexd	|- ( ph -> ( 0 ..^ 2 ) e. _V )
5		s2len	|- ( # ` <" X Y "> ) = 2
6	5	a1i	|- ( ph -> ( # ` <" X Y "> ) = 2 )
7	6	eqcomd	|- ( ph -> 2 = ( # ` <" X Y "> ) )
8	2 3	s2cld	|- ( ph -> <" X Y "> e. Word S )
9	7 8	wrdfd	|- ( ph -> <" X Y "> : ( 0 ..^ 2 ) --> S )
10	1 4 9	elmapdd	|- ( ph -> <" X Y "> e. ( S ^m ( 0 ..^ 2 ) ) )