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 ) )