Theorem hess

Description: Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020)

	Ref	Expression
Assertion	hess	$$⊢S\subseteq R\to \left(RhereditaryA\to ShereditaryA\right)$$

Proof

Step	Hyp	Ref	Expression
1		imass1	$$⊢S\subseteq R\to S\left[A\right]\subseteq R\left[A\right]$$
2		sstr2	$$⊢S\left[A\right]\subseteq R\left[A\right]\to \left(R\left[A\right]\subseteq A\to S\left[A\right]\subseteq A\right)$$
3	1 2	syl	$$⊢S\subseteq R\to \left(R\left[A\right]\subseteq A\to S\left[A\right]\subseteq A\right)$$
4		df-he	$$⊢RhereditaryA\leftrightarrow R\left[A\right]\subseteq A$$
5		df-he	$$⊢ShereditaryA\leftrightarrow S\left[A\right]\subseteq A$$
6	3 4 5	3imtr4g	$$⊢S\subseteq R\to \left(RhereditaryA\to ShereditaryA\right)$$