Theorem singoutnword

Description: Singleton with character out of range V is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024)

	Ref	Expression
Hypothesis	singoutnword.1	|- A e. _V
Assertion	singoutnword	|- ( -. A e. V -> -. <" A "> e. Word V )

Proof

Step	Hyp	Ref	Expression
1		singoutnword.1	|- A e. _V
2		s1fv	|- ( A e. _V -> ( <" A "> ` 0 ) = A )
3	1 2	ax-mp	|- ( <" A "> ` 0 ) = A
4		s1nz	|- <" A "> =/= (/)
5		fstwrdne	|- ( ( <" A "> e. Word V /\ <" A "> =/= (/) ) -> ( <" A "> ` 0 ) e. V )
6	4 5	mpan2	|- ( <" A "> e. Word V -> ( <" A "> ` 0 ) e. V )
7	3 6	eqeltrrid	|- ( <" A "> e. Word V -> A e. V )
8	7	con3i	|- ( -. A e. V -> -. <" A "> e. Word V )