predrelss

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

		Ref	Expression
	Assertion	predrelss	$⊢ R \subseteq S \to Pred (R, A, X) \subseteq Pred (S, A, X)$

Step	Hyp	Ref	Expression
1		cnvss	$⊢ R \subseteq S \to R^{-1} \subseteq S^{-1}$
2		imass1	$⊢ R^{-1} \subseteq S^{-1} \to R^{-1} [\{X\}] \subseteq S^{-1} [\{X\}]$
3		sslin	$⊢ R^{-1} [\{X\}] \subseteq S^{-1} [\{X\}] \to A \cap R^{-1} [\{X\}] \subseteq A \cap S^{-1} [\{X\}]$
4	1 2 3	3syl	$⊢ R \subseteq S \to A \cap R^{-1} [\{X\}] \subseteq A \cap S^{-1} [\{X\}]$
5		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
6		df-pred	$⊢ Pred (S, A, X) = A \cap S^{-1} [\{X\}]$
7	4 5 6	3sstr4g	$⊢ R \subseteq S \to Pred (R, A, X) \subseteq Pred (S, A, X)$

Metamath Proof Explorer