Metamath Proof Explorer


Theorem predrelss

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

Ref Expression
Assertion predrelss RSPredRAXPredSAX

Proof

Step Hyp Ref Expression
1 cnvss RSR-1S-1
2 imass1 R-1S-1R-1XS-1X
3 sslin R-1XS-1XAR-1XAS-1X
4 1 2 3 3syl RSAR-1XAS-1X
5 df-pred PredRAX=AR-1X
6 df-pred PredSAX=AS-1X
7 4 5 6 3sstr4g RSPredRAXPredSAX