Theorem singoutnupword

Description: Singleton with character out of range S is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024)

	Ref	Expression
Hypothesis	singoutnupword.1	|- A e. _V
Assertion	singoutnupword	|- ( -. A e. S -> -. <" A "> e. UpWord S )

Proof

Step	Hyp	Ref	Expression
1		singoutnupword.1	|- A e. _V
2	1	singoutnword	|- ( -. A e. S -> -. <" A "> e. Word S )
3		upwordisword	|- ( <" A "> e. UpWord S -> <" A "> e. Word S )
4	2 3	nsyl	|- ( -. A e. S -> -. <" A "> e. UpWord S )