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	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	s1mapd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion	s1mapd	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ ( 𝑆 ↑m { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		s1mapd.1	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		s1mapd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
3		ovexd	⊢ ( 𝜑 → ( 0 ..^ 1 ) ∈ V )
4		s1len	⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
5	4	a1i	⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1 )
6	5	eqcomd	⊢ ( 𝜑 → 1 = ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) )
7	2	s1cld	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 )
8	6 7	wrdfd	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ : ( 0 ..^ 1 ) ⟶ 𝑆 )
9	1 3 8	elmapdd	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ ( 𝑆 ↑m ( 0 ..^ 1 ) ) )
10		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
11	10	oveq2i	⊢ ( 𝑆 ↑m ( 0 ..^ 1 ) ) = ( 𝑆 ↑m { 0 } )
12	9 11	eleqtrdi	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ ( 𝑆 ↑m { 0 } ) )