Theorem s1chn

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

	Ref	Expression
Hypothesis	s1chn.1	$$⊢\phi \to X\in A$$
Assertion	s1chn	$$⊢\phi \to ⟨“X”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$

Proof

Step	Hyp	Ref	Expression
1		s1chn.1	$$⊢\phi \to X\in A$$
2	1	s1cld	$$⊢\phi \to ⟨“X”⟩\in \mathrm{Word}A$$
3		ral0	$$⊢\forall n\in \varnothing ⟨“X”⟩\left(n-1\right)\underset{\dot{}}{<}⟨“X”⟩\left(n\right)$$
4		s1dm	$$⊢\mathrm{dom}⟨“X”⟩=\left\{0\right\}$$
5	4	difeq1i	$$⊢\mathrm{dom}⟨“X”⟩\setminus \left\{0\right\}=\left\{0\right\}\setminus \left\{0\right\}$$
6		difid	$$⊢\left\{0\right\}\setminus \left\{0\right\}=\varnothing$$
7	5 6	eqtri	$$⊢\mathrm{dom}⟨“X”⟩\setminus \left\{0\right\}=\varnothing$$
8	7	raleqi	$$⊢\forall n\in \left(\mathrm{dom}⟨“X”⟩\setminus \left\{0\right\}\right)⟨“X”⟩\left(n-1\right)\underset{\dot{}}{<}⟨“X”⟩\left(n\right)\leftrightarrow \forall n\in \varnothing ⟨“X”⟩\left(n-1\right)\underset{\dot{}}{<}⟨“X”⟩\left(n\right)$$
9	3 8	mpbir	$$⊢\forall n\in \left(\mathrm{dom}⟨“X”⟩\setminus \left\{0\right\}\right)⟨“X”⟩\left(n-1\right)\underset{\dot{}}{<}⟨“X”⟩\left(n\right)$$
10		ischn	$$⊢⟨“X”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\leftrightarrow \left(⟨“X”⟩\in \mathrm{Word}A\wedge \forall n\in \left(\mathrm{dom}⟨“X”⟩\setminus \left\{0\right\}\right)⟨“X”⟩\left(n-1\right)\underset{\dot{}}{<}⟨“X”⟩\left(n\right)\right)$$
11	2 9 10	sylanblrc	$$⊢\phi \to ⟨“X”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$