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	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	s2mapd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	s2mapd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	s2mapd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ ∈ ( 𝑆 ↑m ( 0 ..^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s2mapd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		s2mapd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
3		s2mapd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
4		ovexd	⊢ ( 𝜑 → ( 0 ..^ 2 ) ∈ V )
5		s2len	⊢ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2
6	5	a1i	⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2 )
7	6	eqcomd	⊢ ( 𝜑 → 2 = ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) )
8	2 3	s2cld	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑆 )
9	7 8	wrdfd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ..^ 2 ) ⟶ 𝑆 )
10	1 4 9	elmapdd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ ∈ ( 𝑆 ↑m ( 0 ..^ 2 ) ) )