Theorem s1chn

Description: A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypothesis	s1chn.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion	s1chn	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ ( < Chain 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		s1chn.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2	1	s1cld	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 )
3		ral0	⊢ ∀ 𝑛 ∈ ∅ ( ⟨“ 𝑋 ”⟩ ‘ ( 𝑛 − 1 ) ) < ( ⟨“ 𝑋 ”⟩ ‘ 𝑛 )
4		s1dm	⊢ dom ⟨“ 𝑋 ”⟩ = { 0 }
5	4	difeq1i	⊢ ( dom ⟨“ 𝑋 ”⟩ ∖ { 0 } ) = ( { 0 } ∖ { 0 } )
6		difid	⊢ ( { 0 } ∖ { 0 } ) = ∅
7	5 6	eqtri	⊢ ( dom ⟨“ 𝑋 ”⟩ ∖ { 0 } ) = ∅
8	7	raleqi	⊢ ( ∀ 𝑛 ∈ ( dom ⟨“ 𝑋 ”⟩ ∖ { 0 } ) ( ⟨“ 𝑋 ”⟩ ‘ ( 𝑛 − 1 ) ) < ( ⟨“ 𝑋 ”⟩ ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ∅ ( ⟨“ 𝑋 ”⟩ ‘ ( 𝑛 − 1 ) ) < ( ⟨“ 𝑋 ”⟩ ‘ 𝑛 ) )
9	3 8	mpbir	⊢ ∀ 𝑛 ∈ ( dom ⟨“ 𝑋 ”⟩ ∖ { 0 } ) ( ⟨“ 𝑋 ”⟩ ‘ ( 𝑛 − 1 ) ) < ( ⟨“ 𝑋 ”⟩ ‘ 𝑛 )
10		ischn	⊢ ( ⟨“ 𝑋 ”⟩ ∈ ( < Chain 𝐴 ) ↔ ( ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom ⟨“ 𝑋 ”⟩ ∖ { 0 } ) ( ⟨“ 𝑋 ”⟩ ‘ ( 𝑛 − 1 ) ) < ( ⟨“ 𝑋 ”⟩ ‘ 𝑛 ) ) )
11	2 9 10	sylanblrc	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ ( < Chain 𝐴 ) )