Metamath Proof Explorer

Theorem chnrdss

Description: Subset theorem for chains. (Contributed by Ender Ting, 20-Jan-2026)

Ref Expression
Assertion chnrdss 
|- ( ( .< C_ R /\ A C_ B ) -> ( .< Chain A ) C_ ( R Chain B ) )

Proof

Step Hyp Ref Expression
1 chnrss 
 |-  ( .< C_ R -> ( .< Chain A ) C_ ( R Chain A ) )
2 chndss 
 |-  ( A C_ B -> ( R Chain A ) C_ ( R Chain B ) )
3 sstr 
 |-  ( ( ( .< Chain A ) C_ ( R Chain A ) /\ ( R Chain A ) C_ ( R Chain B ) ) -> ( .< Chain A ) C_ ( R Chain B ) )
4 1 2 3 syl2an 
 |-  ( ( .< C_ R /\ A C_ B ) -> ( .< Chain A ) C_ ( R Chain B ) )