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	⊢ ( 𝐴 ≠ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nne	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
2		neeq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ↔ 𝐴 ≠ 𝐵 ) )
3	2	biimprcd	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) )
4	1 3	biimtrid	⊢ ( 𝐴 ≠ 𝐵 → ( ¬ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 → ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) )
5	4	orrd	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) )
6		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
7	6	jctl	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) )
8		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
9	8	jctl	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) )
10	7 9	orim12i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ∨ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) ) )
11	5 10	syl	⊢ ( 𝐴 ≠ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ∨ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) ) )
12		ineq2	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) )
13		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
14	12 13	eqtr3di	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
15	14	necon3i	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 → 𝐴 ≠ 𝐵 )
16	15	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) → 𝐴 ≠ 𝐵 )
17		ineq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐵 ) )
18		inidm	⊢ ( 𝐵 ∩ 𝐵 ) = 𝐵
19	17 18	eqtrdi	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
20	19	necon3i	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 → 𝐴 ≠ 𝐵 )
21	20	adantl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
22	16 21	jaoi	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ∨ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) ) → 𝐴 ≠ 𝐵 )
23	11 22	impbii	⊢ ( 𝐴 ≠ 𝐵 ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ∨ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) ) )
24		df-pss	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) )
25		df-pss	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) )
26	24 25	orbi12i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐴 ) ∨ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ≠ 𝐵 ) ) )
27	23 26	bitr4i	⊢ ( 𝐴 ≠ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )