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

Proof

Step	Hyp	Ref	Expression
1		ssbr	|- ( .< C_ R -> ( ( x ` ( c - 1 ) ) .< ( x ` c ) -> ( x ` ( c - 1 ) ) R ( x ` c ) ) )
2	1	ralimdv	|- ( .< C_ R -> ( A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) -> A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) R ( x ` c ) ) )
3	2	anim2d	|- ( .< C_ R -> ( ( x e. Word A /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) .< ( x ` c ) ) -> ( x e. Word A /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) R ( 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. ( R Chain A ) <-> ( x e. Word A /\ A. c e. ( dom x \ { 0 } ) ( x ` ( c - 1 ) ) R ( x ` c ) ) )
6	3 4 5	3imtr4g	|- ( .< C_ R -> ( x e. ( .< Chain A ) -> x e. ( R Chain A ) ) )
7	6	ssrdv	|- ( .< C_ R -> ( .< Chain A ) C_ ( R Chain A ) )