Theorem disjss

Description: Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020) (Revised by Peter Mazsa, 22-Sep-2021)

	Ref	Expression
Assertion	disjss	$$⊢A\subseteq B\to \left(DisjB\to DisjA\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvss	$$⊢A\subseteq B\to A^{-1}\subseteq B^{-1}$$
2		funALTVss	$$⊢A^{-1}\subseteq B^{-1}\to \left(FunALTV{B}^{-1}\to FunALTV{A}^{-1}\right)$$
3	1 2	syl	$$⊢A\subseteq B\to \left(FunALTV{B}^{-1}\to FunALTV{A}^{-1}\right)$$
4		relss	$$⊢A\subseteq B\to \left(\mathrm{Rel}B\to \mathrm{Rel}A\right)$$
5	3 4	anim12d	$$⊢A\subseteq B\to \left(\left(FunALTV{B}^{-1}\wedge \mathrm{Rel}B\right)\to \left(FunALTV{A}^{-1}\wedge \mathrm{Rel}A\right)\right)$$
6		dfdisjALTV	$$⊢DisjB\leftrightarrow \left(FunALTV{B}^{-1}\wedge \mathrm{Rel}B\right)$$
7		dfdisjALTV	$$⊢DisjA\leftrightarrow \left(FunALTV{A}^{-1}\wedge \mathrm{Rel}A\right)$$
8	5 6 7	3imtr4g	$$⊢A\subseteq B\to \left(DisjB\to DisjA\right)$$