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	$$⊢\left(\neg A\subseteq B\wedge C\subseteq B\right)\to \neg A\subseteq C$$

Proof

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