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 (Disj B \to Disj A)$

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

Metamath Proof Explorer