Q:\DJ\DISJOINT.TXT        Revised 1995 October 9     

Theorems about disjointness were introduced 1994 April 4 with the
expectation that the concept of disjointness could be convenient in
the proof of the domain theorems.  But this did not turn out to be
quite as useful as was anticipated.

Definition:

(all x all y (disjoint(x,y) <-> equal(intersection(x,y),0))).

Theorems:

(all x disjoint(x,0)).

(all x disjoint(x,complement(x))).

(all x (disjoint(x,x) <-> equal(x,0))).

(all x all y (disjoint(x,y) -> disjoint(y,x))).

(all x all y (subclass(x,y) <-> disjoint(x,complement(y)))).

(all x all y (-member(x,y) <-> disjoint(singleton(x),y))).

(all x all y all z ((subclass(x,y) & disjoint(y,z)) -> disjoint(x,z))).

(all x all y all z ((disjoint(x,z) & disjoint(y,z)) -> 
                     disjoint(union(x,y),z))).

(all x all y all z (equal(restrict(x,y,z),0) <-> disjoint(x,cart(y,z)))).

Connection to Domain Theorems:

(all z all xr (member(z,D(xr)) <-> (member(z,V) & -disjoint(xr,cart(xr,V))))).

(all xr all y (equal(restrict(xr,y,V),0) -> disjoint(D(xr),y))).

Comments:

While trying to prove DJ-7 it became clear that U-4 had not been included
in the list of available theorems.  How long has that been going on? 

Theorem DJ-10C subsumes lemma DJ-10A.

Theorems DJ-C-1 and DJ-C-2 were added in October 1995 in the course of
proving some results about the relation PS.