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

Proof

Step	Hyp	Ref	Expression
1		ssbr	⊢ ( < ⊆ 𝑅 → ( ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) → ( 𝑥 ‘ ( 𝑐 − 1 ) ) 𝑅 ( 𝑥 ‘ 𝑐 ) ) )
2	1	ralimdv	⊢ ( < ⊆ 𝑅 → ( ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) < ( 𝑥 ‘ 𝑐 ) → ∀ 𝑐 ∈ ( dom 𝑥 ∖ { 0 } ) ( 𝑥 ‘ ( 𝑐 − 1 ) ) 𝑅 ( 𝑥 ‘ 𝑐 ) ) )
3	2	anim2d	⊢ ( < ⊆ 𝑅 → ( ( 𝑥 ∈ 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 𝐴 ) )