Theorem unhe1

Description: The union of two relations hereditary in a class is also hereditary in a class. (Contributed by RP, 28-Mar-2020)

	Ref	Expression
Assertion	unhe1	|- ( ( R hereditary A /\ S hereditary A ) -> ( R u. S ) hereditary A )

Proof

Step	Hyp	Ref	Expression
1		df-he	|- ( R hereditary A <-> ( R " A ) C_ A )
2		df-he	|- ( S hereditary A <-> ( S " A ) C_ A )
3		imaundir	|- ( ( R u. S ) " A ) = ( ( R " A ) u. ( S " A ) )
4		unss	|- ( ( ( R " A ) C_ A /\ ( S " A ) C_ A ) <-> ( ( R " A ) u. ( S " A ) ) C_ A )
5	4	biimpi	|- ( ( ( R " A ) C_ A /\ ( S " A ) C_ A ) -> ( ( R " A ) u. ( S " A ) ) C_ A )
6	3 5	eqsstrid	|- ( ( ( R " A ) C_ A /\ ( S " A ) C_ A ) -> ( ( R u. S ) " A ) C_ A )
7	1 2 6	syl2anb	|- ( ( R hereditary A /\ S hereditary A ) -> ( ( R u. S ) " A ) C_ A )
8		df-he	|- ( ( R u. S ) hereditary A <-> ( ( R u. S ) " A ) C_ A )
9	7 8	sylibr	|- ( ( R hereditary A /\ S hereditary A ) -> ( R u. S ) hereditary A )