Theorem chnrss

Description: Chains under a relation are also chains under any superset relation. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chnrss	$$⊢\underset{\dot{}}{<}\subseteq R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{A}R$$

Proof

Step	Hyp	Ref	Expression
1		ssbr	$$⊢\underset{\dot{}}{<}\subseteq R\to \left(x\left(c-1\right)\underset{\dot{}}{<}x\left(c\right)\to x\left(c-1\right)Rx\left(c\right)\right)$$
2	1	ralimdv	$$⊢\underset{\dot{}}{<}\subseteq R\to \left(\forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)\underset{\dot{}}{<}x\left(c\right)\to \forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)Rx\left(c\right)\right)$$
3	2	anim2d	$$⊢\underset{\dot{}}{<}\subseteq R\to \left(\left(x\in \mathrm{Word}A\wedge \forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)\underset{\dot{}}{<}x\left(c\right)\right)\to \left(x\in \mathrm{Word}A\wedge \forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)Rx\left(c\right)\right)\right)$$
4		ischn	$$⊢x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\leftrightarrow \left(x\in \mathrm{Word}A\wedge \forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)\underset{\dot{}}{<}x\left(c\right)\right)$$
5		ischn	$$⊢x\in {\mathrm{Chain}}_{A}R\leftrightarrow \left(x\in \mathrm{Word}A\wedge \forall c\in \left(\mathrm{dom}x\setminus \left\{0\right\}\right)x\left(c-1\right)Rx\left(c\right)\right)$$
6	3 4 5	3imtr4g	$$⊢\underset{\dot{}}{<}\subseteq R\to \left(x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to x\in {\mathrm{Chain}}_{A}R\right)$$
7	6	ssrdv	$$⊢\underset{\dot{}}{<}\subseteq R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{A}R$$