Theorem s1dm

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

	Ref	Expression
Assertion	s1dm	|- dom <" A "> = { 0 }

Proof

Step	Hyp	Ref	Expression
1		s1cli	|- <" A "> e. Word _V
2		wrdf	|- ( <" A "> e. Word _V -> <" A "> : ( 0 ..^ ( # ` <" A "> ) ) --> _V )
3	1 2	ax-mp	|- <" A "> : ( 0 ..^ ( # ` <" A "> ) ) --> _V
4		s1len	|- ( # ` <" A "> ) = 1
5		oveq2	|- ( ( # ` <" A "> ) = 1 -> ( 0 ..^ ( # ` <" A "> ) ) = ( 0 ..^ 1 ) )
6		fzo01	|- ( 0 ..^ 1 ) = { 0 }
7	5 6	eqtrdi	|- ( ( # ` <" A "> ) = 1 -> ( 0 ..^ ( # ` <" A "> ) ) = { 0 } )
8	4 7	ax-mp	|- ( 0 ..^ ( # ` <" A "> ) ) = { 0 }
9	8	eqcomi	|- { 0 } = ( 0 ..^ ( # ` <" A "> ) )
10	9	feq2i	|- ( <" A "> : { 0 } --> _V <-> <" A "> : ( 0 ..^ ( # ` <" A "> ) ) --> _V )
11	3 10	mpbir	|- <" A "> : { 0 } --> _V
12	11	fdmi	|- dom <" A "> = { 0 }