THEOREM

*******

 

       ALL(a):ALL(b):ALL(c):[Set(a) & Set(b) & Set(c)

       => [b<=a & c<=a => b-c=b+(a-c)]]

 

       where '<=' is the subset relation,  '+' is the intersection operator, '-' is set subtraction

 

 

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

 

DEFINITIONS

***********

 

Define: +

 

x+y = the intersection of sets x and y

 

1     ALL(a):ALL(b):[Set(a) & Set(b) => Set(a+b) & ALL(c):[c e a+b <=> c e a & c e b]]

      Axiom

 

 

Define: *

 

x*y = the union of sets x and y

 

2     ALL(a):ALL(b):[Set(a) & Set(b) => Set(a*b) & ALL(c):[c e a*b <=> c e a | c e b]]

      Axiom

 

 

Define: -

 

x-y = the complement of set y wrt set x (i.e. the elements of set y "subtracted" from set x)

 

3     ALL(a):ALL(b):[Set(a) & Set(b) => Set(a-b) & ALL(c):[c e a-b <=> c e a & ~c e b]]

      Axiom

 

 

Define: <=

 

x<=y means the set x is a subset of set y

 

4     ALL(a):ALL(b):[Set(a) & Set(b) => [a<=b <=> ALL(c):[c e a => c e b]]]

      Axiom

 

   

    PROOF

    *****

   

    Suppose...

 

      5     Set(u) & Set(x) & Set(y)

            Premise

 

      6     Set(u)

            Split, 5

 

      7     Set(x)

            Split, 5

 

      8     Set(y)

            Split, 5

 

        

         Prove: x<=u & y<=u => x-y=x+(u-y)

        

         Suppose...

 

            9     x<=u & y<=u

                  Premise

 

            10   x<=u

                  Split, 9

 

            11   y<=u

                  Split, 9

 

         Apply Set Equality Axiom

 

            12   ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

                  Set Equality

 

            13   ALL(b):[Set(x-y) & Set(b) => [x-y=b <=> ALL(c):[c e x-y <=> c e b]]]

                  U Spec, 12

 

            14   Set(x-y) & Set(x+(u-y)) => [x-y=x+(u-y) <=> ALL(c):[c e x-y <=> c e x+(u-y)]]

                  U Spec, 13

 

            15   ALL(b):[Set(x) & Set(b) => Set(x-b) & ALL(c):[c e x-b <=> c e x & ~c e b]]

                  U Spec, 3

 

            16   Set(x) & Set(y) => Set(x-y) & ALL(c):[c e x-y <=> c e x & ~c e y]

                  U Spec, 15

 

            17   Set(x) & Set(y)

                  Join, 7, 8

 

            18   Set(x-y) & ALL(c):[c e x-y <=> c e x & ~c e y]

                  Detach, 16, 17

 

            19   Set(x-y)

                  Split, 18

 

            20   ALL(c):[c e x-y <=> c e x & ~c e y]

                  Split, 18

 

         Apply definition of intersection (+)

 

            21   ALL(b):[Set(x) & Set(b) => Set(x+b) & ALL(c):[c e x+b <=> c e x & c e b]]

                  U Spec, 1

 

            22   Set(x) & Set(u-y) => Set(x+(u-y)) & ALL(c):[c e x+(u-y) <=> c e x & c e u-y]

                  U Spec, 21

 

         Apply definition of set subtraction

 

            23   ALL(b):[Set(u) & Set(b) => Set(u-b) & ALL(c):[c e u-b <=> c e u & ~c e b]]

                  U Spec, 3

 

            24   Set(u) & Set(y) => Set(u-y) & ALL(c):[c e u-y <=> c e u & ~c e y]

                  U Spec, 23

 

            25   Set(u) & Set(y)

                  Join, 6, 8

 

            26   Set(u-y) & ALL(c):[c e u-y <=> c e u & ~c e y]

                  Detach, 24, 25

 

            27   Set(u-y)

                  Split, 26

 

            28   ALL(c):[c e u-y <=> c e u & ~c e y]

                  Split, 26

 

            29   Set(x) & Set(u-y)

                  Join, 7, 27

 

            30   Set(x+(u-y)) & ALL(c):[c e x+(u-y) <=> c e x & c e u-y]

                  Detach, 22, 29

 

            31   Set(x+(u-y))

                  Split, 30

 

            32   ALL(c):[c e x+(u-y) <=> c e x & c e u-y]

                  Split, 30

 

            33   Set(x-y) & Set(x+(u-y))

                  Join, 19, 31

 

            34   x-y=x+(u-y) <=> ALL(c):[c e x-y <=> c e x+(u-y)]

                  Detach, 14, 33

 

            35   [x-y=x+(u-y) => ALL(c):[c e x-y <=> c e x+(u-y)]]

             & [ALL(c):[c e x-y <=> c e x+(u-y)] => x-y=x+(u-y)]

                  Iff-And, 34

 

            36   x-y=x+(u-y) => ALL(c):[c e x-y <=> c e x+(u-y)]

                  Split, 35

 

         Sufficient: For x-y=x+(u-y)

 

            37   ALL(c):[c e x-y <=> c e x+(u-y)] => x-y=x+(u-y)

                  Split, 35

 

            

             '=>'

            

             Prove: ALL(c):[c e x-y => c e x+(u-y)]

            

             Suppose...

 

                  38   t e x-y

                        Premise

 

             From defintion of set subtraction...

 

                  39   t e x-y <=> t e x & ~t e y

                        U Spec, 20

 

                  40   [t e x-y => t e x & ~t e y]

                 & [t e x & ~t e y => t e x-y]

                        Iff-And, 39

 

                  41   t e x-y => t e x & ~t e y

                        Split, 40

 

                  42   t e x & ~t e y => t e x-y

                        Split, 40

 

                  43   t e x & ~t e y

                        Detach, 41, 38

 

                  44   t e x

                        Split, 43

 

                  45   ~t e y

                        Split, 43

 

             Apply previous result

 

                  46   t e x+(u-y) <=> t e x & t e u-y

                        U Spec, 32

 

                  47   [t e x+(u-y) => t e x & t e u-y]

                 & [t e x & t e u-y => t e x+(u-y)]

                        Iff-And, 46

 

                  48   t e x+(u-y) => t e x & t e u-y

                        Split, 47

 

             Sufficient: For t e x+(u-y)

 

                  49   t e x & t e u-y => t e x+(u-y)

                        Split, 47

 

             From definition of set subtraction...

 

                  50   t e u-y <=> t e u & ~t e y

                        U Spec, 28

 

                  51   [t e u-y => t e u & ~t e y]

                 & [t e u & ~t e y => t e u-y]

                        Iff-And, 50

 

                  52   t e u-y => t e u & ~t e y

                        Split, 51

 

             Sufficient: For t e u-y

 

                  53   t e u & ~t e y => t e u-y

                        Split, 51

 

             Apply definition of subset (<=)

 

                  54   ALL(b):[Set(x) & Set(b) => [x<=b <=> ALL(c):[c e x => c e b]]]

                        U Spec, 4

 

                  55   Set(x) & Set(u) => [x<=u <=> ALL(c):[c e x => c e u]]

                        U Spec, 54

 

                  56   Set(x) & Set(u)

                        Join, 7, 6

 

                  57   x<=u <=> ALL(c):[c e x => c e u]

                        Detach, 55, 56

 

                  58   [x<=u => ALL(c):[c e x => c e u]]

                 & [ALL(c):[c e x => c e u] => x<=u]

                        Iff-And, 57

 

                  59   x<=u => ALL(c):[c e x => c e u]

                        Split, 58

 

                  60   ALL(c):[c e x => c e u] => x<=u

                        Split, 58

 

                  61   ALL(c):[c e x => c e u]

                        Detach, 59, 10

 

                  62   t e x => t e u

                        U Spec, 61

 

                  63   t e u

                        Detach, 62, 44

 

                  64   t e u & ~t e y

                        Join, 63, 45

 

                  65   t e u-y

                        Detach, 53, 64

 

                  66   t e x & t e u-y

                        Join, 44, 65

 

                  67   t e x+(u-y)

                        Detach, 49, 66

 

        

         '=>'

        

         As Required:

 

            68   ALL(c):[c e x-y => c e x+(u-y)]

                  4 Conclusion, 38

 

            

             '<='

            

             Prove: ALL(c):[c e x+(u-y) => c e x-y]

            

             Suppose...

 

                  69   t e x+(u-y)

                        Premise

 

             Apply previous result

 

                  70   t e x+(u-y) <=> t e x & t e u-y

                        U Spec, 32

 

                  71   [t e x+(u-y) => t e x & t e u-y]

                 & [t e x & t e u-y => t e x+(u-y)]

                        Iff-And, 70

 

                  72   t e x+(u-y) => t e x & t e u-y

                        Split, 71

 

                  73   t e x & t e u-y => t e x+(u-y)

                        Split, 71

 

                  74   t e x & t e u-y

                        Detach, 72, 69

 

                  75   t e x

                        Split, 74

 

                  76   t e u-y

                        Split, 74

 

             From definition of set subtraction...

 

                  77   t e u-y <=> t e u & ~t e y

                        U Spec, 28

 

                  78   [t e u-y => t e u & ~t e y]

                 & [t e u & ~t e y => t e u-y]

                        Iff-And, 77

 

                  79   t e u-y => t e u & ~t e y

                        Split, 78

 

                  80   t e u & ~t e y => t e u-y

                        Split, 78

 

                  81   t e u & ~t e y

                        Detach, 79, 76

 

                  82   t e u

                        Split, 81

 

                  83   ~t e y

                        Split, 81

 

             From definition of set subtraction...

 

                  84   t e x-y <=> t e x & ~t e y

                        U Spec, 20

 

                  85   [t e x-y => t e x & ~t e y]

                 & [t e x & ~t e y => t e x-y]

                        Iff-And, 84

 

                  86   t e x-y => t e x & ~t e y

                        Split, 85

 

             Sufficient: For t e x-y

 

                  87   t e x & ~t e y => t e x-y

                        Split, 85

 

                  88   t e x & ~t e y

                        Join, 75, 83

 

                  89   t e x-y

                        Detach, 87, 88

 

         As Required:

 

            90   ALL(c):[c e x+(u-y) => c e x-y]

                  4 Conclusion, 69

 

            91   ALL(c):[[c e x-y => c e x+(u-y)] & [c e x+(u-y) => c e x-y]]

                  Join, 68, 90

 

            92   ALL(c):[c e x-y <=> c e x+(u-y)]

                  Iff-And, 91

 

            93   x-y=x+(u-y)

                  Detach, 37, 92

 

    As Required:

 

      94   x<=u & y<=u => x-y=x+(u-y)

            4 Conclusion, 9

 

As Required:

 

95   ALL(a):ALL(b):ALL(c):[Set(a) & Set(b) & Set(c)

    => [b<=a & c<=a => b-c=b+(a-c)]]

      4 Conclusion, 5