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	$$⊢\left(RhereditaryA\wedge ShereditaryA\right)\to \left(R\cup S\right)hereditaryA$$

Proof

Step	Hyp	Ref	Expression
1		df-he	$$⊢RhereditaryA\leftrightarrow R\left[A\right]\subseteq A$$
2		df-he	$$⊢ShereditaryA\leftrightarrow S\left[A\right]\subseteq A$$
3		imaundir	$$⊢\left(R\cup S\right)\left[A\right]=R\left[A\right]\cup S\left[A\right]$$
4		unss	$$⊢\left(R\left[A\right]\subseteq A\wedge S\left[A\right]\subseteq A\right)\leftrightarrow R\left[A\right]\cup S\left[A\right]\subseteq A$$
5	4	biimpi	$$⊢\left(R\left[A\right]\subseteq A\wedge S\left[A\right]\subseteq A\right)\to R\left[A\right]\cup S\left[A\right]\subseteq A$$
6	3 5	eqsstrid	$$⊢\left(R\left[A\right]\subseteq A\wedge S\left[A\right]\subseteq A\right)\to \left(R\cup S\right)\left[A\right]\subseteq A$$
7	1 2 6	syl2anb	$$⊢\left(RhereditaryA\wedge ShereditaryA\right)\to \left(R\cup S\right)\left[A\right]\subseteq A$$
8		df-he	$$⊢\left(R\cup S\right)hereditaryA\leftrightarrow \left(R\cup S\right)\left[A\right]\subseteq A$$
9	7 8	sylibr	$$⊢\left(RhereditaryA\wedge ShereditaryA\right)\to \left(R\cup S\right)hereditaryA$$