This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem predrelss

Description: Subset carries from relation to predecessor class. (Contributed by Scott Fenton, 25-Nov-2024)

Ref Expression
Assertion predrelss 
|- ( R C_ S -> Pred ( R , A , X ) C_ Pred ( S , A , X ) )

Proof

Step Hyp Ref Expression
1 cnvss 
 |-  ( R C_ S -> `' R C_ `' S )
2 imass1 
 |-  ( `' R C_ `' S -> ( `' R " { X } ) C_ ( `' S " { X } ) )
3 sslin 
 |-  ( ( `' R " { X } ) C_ ( `' S " { X } ) -> ( A i^i ( `' R " { X } ) ) C_ ( A i^i ( `' S " { X } ) ) )
4 1 2 3 3syl 
 |-  ( R C_ S -> ( A i^i ( `' R " { X } ) ) C_ ( A i^i ( `' S " { X } ) ) )
5 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
6 df-pred 
 |-  Pred ( S , A , X ) = ( A i^i ( `' S " { X } ) )
7 4 5 6 3sstr4g 
 |-  ( R C_ S -> Pred ( R , A , X ) C_ Pred ( S , A , X ) )