Theorem chnrdss

Description: Subset theorem for chains. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chnrdss	$$⊢\left(\underset{\dot{}}{<}\subseteq R\wedge A\subseteq B\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{B}R$$

Proof

Step	Hyp	Ref	Expression
1		chnrss	$$⊢\underset{\dot{}}{<}\subseteq R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{A}R$$
2		chndss	$$⊢A\subseteq B\to {\mathrm{Chain}}_{A}R\subseteq {\mathrm{Chain}}_{B}R$$
3		sstr	$$⊢\left({\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{A}R\wedge {\mathrm{Chain}}_{A}R\subseteq {\mathrm{Chain}}_{B}R\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{B}R$$
4	1 2 3	syl2an	$$⊢\left(\underset{\dot{}}{<}\subseteq R\wedge A\subseteq B\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_{B}R$$