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 S Pred R A X Pred S A X

Proof

Step Hyp Ref Expression
1 cnvss R S R -1 S -1
2 imass1 R -1 S -1 R -1 X S -1 X
3 sslin R -1 X S -1 X A R -1 X A S -1 X
4 1 2 3 3syl R S A R -1 X A S -1 X
5 df-pred Pred R A X = A R -1 X
6 df-pred Pred S A X = A S -1 X
7 4 5 6 3sstr4g R S Pred R A X Pred S A X