Theorem chndss

Description: Chains with an alphabet are also chains with any superset alphabet. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chndss	$$⊢A\subseteq B\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_B\underset{\dot{}}{<}$$

Proof

Step	Hyp	Ref	Expression
1		sswrd	$$⊢A\subseteq B\to \mathrm{Word}A\subseteq \mathrm{Word}B$$
2	1	sseld	$$⊢A\subseteq B\to \left(x\in \mathrm{Word}A\to x\in \mathrm{Word}B\right)$$
3	2	anim1d	$$⊢A\subseteq B\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}B\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)\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}}_B\underset{\dot{}}{<}\leftrightarrow \left(x\in \mathrm{Word}B\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)$$
6	3 4 5	3imtr4g	$$⊢A\subseteq B\to \left(x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to x\in {\mathrm{Chain}}_B\underset{\dot{}}{<}\right)$$
7	6	ssrdv	$$⊢A\subseteq B\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq {\mathrm{Chain}}_B\underset{\dot{}}{<}$$