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	⊢ 𝐴 ∈ V
Assertion	singoutnword	⊢ ( ¬ 𝐴 ∈ 𝑉 → ¬ ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		singoutnword.1	⊢ 𝐴 ∈ V
2		s1fv	⊢ ( 𝐴 ∈ V → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴 )
3	1 2	ax-mp	⊢ ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴
4		s1nz	⊢ ⟨“ 𝐴 ”⟩ ≠ ∅
5		fstwrdne	⊢ ( ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐴 ”⟩ ≠ ∅ ) → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) ∈ 𝑉 )
6	4 5	mpan2	⊢ ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) ∈ 𝑉 )
7	3 6	eqeltrrid	⊢ ( ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 → 𝐴 ∈ 𝑉 )
8	7	con3i	⊢ ( ¬ 𝐴 ∈ 𝑉 → ¬ ⟨“ 𝐴 ”⟩ ∈ Word 𝑉 )