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	⊢ ( 𝐴 ⊆ 𝐵 → ( < Chain 𝐴 ) ⊆ ( < Chain 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sswrd	⊢ ( 𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵 )
2	1	sseld	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ Word 𝐴 → 𝑥 ∈ Word 𝐵 ) )
3	2	anim1d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ Word 𝐴 ∧ ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) ) → ( 𝑥 ∈ Word 𝐵 ∧ ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) ) ) )
4		ischn	⊢ ( 𝑥 ∈ ( < Chain 𝐴 ) ↔ ( 𝑥 ∈ Word 𝐴 ∧ ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) ) )
5		ischn	⊢ ( 𝑥 ∈ ( < Chain 𝐵 ) ↔ ( 𝑥 ∈ Word 𝐵 ∧ ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) ) )
6	3 4 5	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ ( < Chain 𝐴 ) → 𝑥 ∈ ( < Chain 𝐵 ) ) )
7	6	ssrdv	⊢ ( 𝐴 ⊆ 𝐵 → ( < Chain 𝐴 ) ⊆ ( < Chain 𝐵 ) )