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	⊢ 𝐴 ∈ V
Assertion	singoutnupword	⊢ ( ¬ 𝐴 ∈ 𝑆 → ¬ ⟨“ 𝐴 ”⟩ ∈ UpWord 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		singoutnupword.1	⊢ 𝐴 ∈ V
2	1	singoutnword	⊢ ( ¬ 𝐴 ∈ 𝑆 → ¬ ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 )
3		upwordisword	⊢ ( ⟨“ 𝐴 ”⟩ ∈ UpWord 𝑆 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑆 )
4	2 3	nsyl	⊢ ( ¬ 𝐴 ∈ 𝑆 → ¬ ⟨“ 𝐴 ”⟩ ∈ UpWord 𝑆 )