Theorem nepss

Description: Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011)

	Ref	Expression
Assertion	nepss	$$⊢A\ne B\leftrightarrow \left(A\cap B\subset A\vee A\cap B\subset B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nne	$$⊢\neg A\cap B\ne A\leftrightarrow A\cap B=A$$
2		neeq1	$$⊢A\cap B=A\to \left(A\cap B\ne B\leftrightarrow A\ne B\right)$$
3	2	biimprcd	$$⊢A\ne B\to \left(A\cap B=A\to A\cap B\ne B\right)$$
4	1 3	biimtrid	$$⊢A\ne B\to \left(\neg A\cap B\ne A\to A\cap B\ne B\right)$$
5	4	orrd	$$⊢A\ne B\to \left(A\cap B\ne A\vee A\cap B\ne B\right)$$
6		inss1	$$⊢A\cap B\subseteq A$$
7	6	jctl	$$⊢A\cap B\ne A\to \left(A\cap B\subseteq A\wedge A\cap B\ne A\right)$$
8		inss2	$$⊢A\cap B\subseteq B$$
9	8	jctl	$$⊢A\cap B\ne B\to \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)$$
10	7 9	orim12i	$$⊢\left(A\cap B\ne A\vee A\cap B\ne B\right)\to \left(\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\vee \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\right)$$
11	5 10	syl	$$⊢A\ne B\to \left(\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\vee \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\right)$$
12		ineq2	$$⊢A=B\to A\cap A=A\cap B$$
13		inidm	$$⊢A\cap A=A$$
14	12 13	eqtr3di	$$⊢A=B\to A\cap B=A$$
15	14	necon3i	$$⊢A\cap B\ne A\to A\ne B$$
16	15	adantl	$$⊢\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\to A\ne B$$
17		ineq1	$$⊢A=B\to A\cap B=B\cap B$$
18		inidm	$$⊢B\cap B=B$$
19	17 18	eqtrdi	$$⊢A=B\to A\cap B=B$$
20	19	necon3i	$$⊢A\cap B\ne B\to A\ne B$$
21	20	adantl	$$⊢\left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\to A\ne B$$
22	16 21	jaoi	$$⊢\left(\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\vee \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\right)\to A\ne B$$
23	11 22	impbii	$$⊢A\ne B\leftrightarrow \left(\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\vee \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\right)$$
24		df-pss	$$⊢A\cap B\subset A\leftrightarrow \left(A\cap B\subseteq A\wedge A\cap B\ne A\right)$$
25		df-pss	$$⊢A\cap B\subset B\leftrightarrow \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)$$
26	24 25	orbi12i	$$⊢\left(A\cap B\subset A\vee A\cap B\subset B\right)\leftrightarrow \left(\left(A\cap B\subseteq A\wedge A\cap B\ne A\right)\vee \left(A\cap B\subseteq B\wedge A\cap B\ne B\right)\right)$$
27	23 26	bitr4i	$$⊢A\ne B\leftrightarrow \left(A\cap B\subset A\vee A\cap B\subset B\right)$$