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	⊢ ( ( 𝑅 hereditary 𝐴 ∧ 𝑆 hereditary 𝐴 ) → ( 𝑅 ∪ 𝑆 ) hereditary 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-he	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
2		df-he	⊢ ( 𝑆 hereditary 𝐴 ↔ ( 𝑆 “ 𝐴 ) ⊆ 𝐴 )
3		imaundir	⊢ ( ( 𝑅 ∪ 𝑆 ) “ 𝐴 ) = ( ( 𝑅 “ 𝐴 ) ∪ ( 𝑆 “ 𝐴 ) )
4		unss	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑆 “ 𝐴 ) ⊆ 𝐴 ) ↔ ( ( 𝑅 “ 𝐴 ) ∪ ( 𝑆 “ 𝐴 ) ) ⊆ 𝐴 )
5	4	biimpi	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑆 “ 𝐴 ) ⊆ 𝐴 ) → ( ( 𝑅 “ 𝐴 ) ∪ ( 𝑆 “ 𝐴 ) ) ⊆ 𝐴 )
6	3 5	eqsstrid	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑆 “ 𝐴 ) ⊆ 𝐴 ) → ( ( 𝑅 ∪ 𝑆 ) “ 𝐴 ) ⊆ 𝐴 )
7	1 2 6	syl2anb	⊢ ( ( 𝑅 hereditary 𝐴 ∧ 𝑆 hereditary 𝐴 ) → ( ( 𝑅 ∪ 𝑆 ) “ 𝐴 ) ⊆ 𝐴 )
8		df-he	⊢ ( ( 𝑅 ∪ 𝑆 ) hereditary 𝐴 ↔ ( ( 𝑅 ∪ 𝑆 ) “ 𝐴 ) ⊆ 𝐴 )
9	7 8	sylibr	⊢ ( ( 𝑅 hereditary 𝐴 ∧ 𝑆 hereditary 𝐴 ) → ( 𝑅 ∪ 𝑆 ) hereditary 𝐴 )