Theorem hess

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

	Ref	Expression
Assertion	hess	|- ( S C_ R -> ( R hereditary A -> S hereditary A ) )

Proof

Step	Hyp	Ref	Expression
1		imass1	|- ( S C_ R -> ( S " A ) C_ ( R " A ) )
2		sstr2	|- ( ( S " A ) C_ ( R " A ) -> ( ( R " A ) C_ A -> ( S " A ) C_ A ) )
3	1 2	syl	|- ( S C_ R -> ( ( R " A ) C_ A -> ( S " A ) C_ A ) )
4		df-he	|- ( R hereditary A <-> ( R " A ) C_ A )
5		df-he	|- ( S hereditary A <-> ( S " A ) C_ A )
6	3 4 5	3imtr4g	|- ( S C_ R -> ( R hereditary A -> S hereditary A ) )