This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nsstr

Description: If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Assertion	nsstr	$⊢ (\neg A \subseteq B \land C \subseteq B) \to \neg A \subseteq C$

Step	Hyp	Ref	Expression
1		sstr	$⊢ (A \subseteq C \land C \subseteq B) \to A \subseteq B$
2	1	ancoms	$⊢ (C \subseteq B \land A \subseteq C) \to A \subseteq B$
3	2	adantll	$⊢ ((\neg A \subseteq B \land C \subseteq B) \land A \subseteq C) \to A \subseteq B$
4		simpll	$⊢ ((\neg A \subseteq B \land C \subseteq B) \land A \subseteq C) \to \neg A \subseteq B$
5	3 4	pm2.65da	$⊢ (\neg A \subseteq B \land C \subseteq B) \to \neg A \subseteq C$