Theorem s1dm

Description: The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020)

	Ref	Expression
Assertion	s1dm	⊢ dom ⟨“ 𝐴 ”⟩ = { 0 }

Proof

Step	Hyp	Ref	Expression
1		s1cli	⊢ ⟨“ 𝐴 ”⟩ ∈ Word V
2		wrdf	⊢ ( ⟨“ 𝐴 ”⟩ ∈ Word V → ⟨“ 𝐴 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ⟶ V )
3	1 2	ax-mp	⊢ ⟨“ 𝐴 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ⟶ V
4		s1len	⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
5		oveq2	⊢ ( ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 → ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = ( 0 ..^ 1 ) )
6		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
7	5 6	eqtrdi	⊢ ( ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 → ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = { 0 } )
8	4 7	ax-mp	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = { 0 }
9	8	eqcomi	⊢ { 0 } = ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) )
10	9	feq2i	⊢ ( ⟨“ 𝐴 ”⟩ : { 0 } ⟶ V ↔ ⟨“ 𝐴 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ⟶ V )
11	3 10	mpbir	⊢ ⟨“ 𝐴 ”⟩ : { 0 } ⟶ V
12	11	fdmi	⊢ dom ⟨“ 𝐴 ”⟩ = { 0 }