Metamath Proof Explorer

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 =/= B <-> ( ( A i^i B ) C. A \/ ( A i^i B ) C. B ) )

Proof

Step Hyp Ref Expression
1 nne 
 |-  ( -. ( A i^i B ) =/= A <-> ( A i^i B ) = A )
2 neeq1 
 |-  ( ( A i^i B ) = A -> ( ( A i^i B ) =/= B <-> A =/= B ) )
3 2 biimprcd 
 |-  ( A =/= B -> ( ( A i^i B ) = A -> ( A i^i B ) =/= B ) )
4 1 3 syl5bi 
 |-  ( A =/= B -> ( -. ( A i^i B ) =/= A -> ( A i^i B ) =/= B ) )
5 4 orrd 
 |-  ( A =/= B -> ( ( A i^i B ) =/= A \/ ( A i^i B ) =/= B ) )
6 inss1 
 |-  ( A i^i B ) C_ A
7 6 jctl 
 |-  ( ( A i^i B ) =/= A -> ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) )
8 inss2 
 |-  ( A i^i B ) C_ B
9 8 jctl 
 |-  ( ( A i^i B ) =/= B -> ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) )
10 7 9 orim12i 
 |-  ( ( ( A i^i B ) =/= A \/ ( A i^i B ) =/= B ) -> ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) \/ ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) ) )
11 5 10 syl 
 |-  ( A =/= B -> ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) \/ ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) ) )
12 ineq2 
 |-  ( A = B -> ( A i^i A ) = ( A i^i B ) )
13 inidm 
 |-  ( A i^i A ) = A
14 12 13 eqtr3di 
 |-  ( A = B -> ( A i^i B ) = A )
15 14 necon3i 
 |-  ( ( A i^i B ) =/= A -> A =/= B )
16 15 adantl 
 |-  ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) -> A =/= B )
17 ineq1 
 |-  ( A = B -> ( A i^i B ) = ( B i^i B ) )
18 inidm 
 |-  ( B i^i B ) = B
19 17 18 eqtrdi 
 |-  ( A = B -> ( A i^i B ) = B )
20 19 necon3i 
 |-  ( ( A i^i B ) =/= B -> A =/= B )
21 20 adantl 
 |-  ( ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) -> A =/= B )
22 16 21 jaoi 
 |-  ( ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) \/ ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) ) -> A =/= B )
23 11 22 impbii 
 |-  ( A =/= B <-> ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) \/ ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) ) )
24 df-pss 
 |-  ( ( A i^i B ) C. A <-> ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) )
25 df-pss 
 |-  ( ( A i^i B ) C. B <-> ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) )
26 24 25 orbi12i 
 |-  ( ( ( A i^i B ) C. A \/ ( A i^i B ) C. B ) <-> ( ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) \/ ( ( A i^i B ) C_ B /\ ( A i^i B ) =/= B ) ) )
27 23 26 bitr4i 
 |-  ( A =/= B <-> ( ( A i^i B ) C. A \/ ( A i^i B ) C. B ) )