Theorem snopiswrd

Description: A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018) (Proof shortened by AV, 18-Apr-2021)

	Ref	Expression
Assertion	snopiswrd	|- ( S e. V -> { <. 0 , S >. } e. Word V )

Proof

Step	Hyp	Ref	Expression
1		0zd	|- ( S e. V -> 0 e. ZZ )
2		id	|- ( S e. V -> S e. V )
3	1 2	fsnd	|- ( S e. V -> { <. 0 , S >. } : { 0 } --> V )
4		fzo01	|- ( 0 ..^ 1 ) = { 0 }
5	4	feq2i	|- ( { <. 0 , S >. } : ( 0 ..^ 1 ) --> V <-> { <. 0 , S >. } : { 0 } --> V )
6	3 5	sylibr	|- ( S e. V -> { <. 0 , S >. } : ( 0 ..^ 1 ) --> V )
7		iswrdi	|- ( { <. 0 , S >. } : ( 0 ..^ 1 ) --> V -> { <. 0 , S >. } e. Word V )
8	6 7	syl	|- ( S e. V -> { <. 0 , S >. } e. Word V )