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 C_ B -> ( .< Chain A ) C_ ( .< Chain B ) )

Proof

Step	Hyp	Ref	Expression
1		sswrd	|- ( A C_ B -> Word A C_ Word B )
2	1	sseld	|- ( A C_ B -> ( x e. Word A -> x e. Word B ) )
3	2	anim1d	|- ( A C_ B -> ( ( x e. Word A /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) ) -> ( x e. Word B /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) ) ) )
4		ischn	|- ( x e. ( .< Chain A ) <-> ( x e. Word A /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) ) )
5		ischn	|- ( x e. ( .< Chain B ) <-> ( x e. Word B /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) ) )
6	3 4 5	3imtr4g	|- ( A C_ B -> ( x e. ( .< Chain A ) -> x e. ( .< Chain B ) ) )
7	6	ssrdv	|- ( A C_ B -> ( .< Chain A ) C_ ( .< Chain B ) )