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	$$⊢\phi \to S\in V$$
	s2mapd.x	$$⊢\phi \to X\in S$$
	s2mapd.y	$$⊢\phi \to Y\in S$$
Assertion	s2mapd	$$⊢\phi \to ⟨“XY”⟩\in \left(S^{\left(0..^2\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		s2mapd.s	$$⊢\phi \to S\in V$$
2		s2mapd.x	$$⊢\phi \to X\in S$$
3		s2mapd.y	$$⊢\phi \to Y\in S$$
4		ovexd	$$⊢\phi \to \left(0..^2\right)\in \mathrm{V}$$
5		s2len	$$⊢\left|⟨“XY”⟩\right|=2$$
6	5	a1i	$$⊢\phi \to \left|⟨“XY”⟩\right|=2$$
7	6	eqcomd	$$⊢\phi \to 2=\left|⟨“XY”⟩\right|$$
8	2 3	s2cld	$$⊢\phi \to ⟨“XY”⟩\in \mathrm{Word}S$$
9	7 8	wrdfd	$$⊢\phi \to ⟨“XY”⟩:\left(0..^2\right)⟶S$$
10	1 4 9	elmapdd	$$⊢\phi \to ⟨“XY”⟩\in \left(S^{\left(0..^2\right)}\right)$$