THEOREM

*******

 

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

 

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

 

 

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(x) & Set(y)

            Premise

 

      6     Set(x)

            Split, 5

 

      7     Set(y)

            Split, 5

 

    Apply definition of subset (<=)

 

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

            U Spec, 4

 

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

            U Spec, 8

 

    Apply definition of intersection (+)

 

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

            U Spec, 1

 

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

            U Spec, 10

 

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

            Detach, 11, 5

 

      13   Set(x+y)

            Split, 12

 

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

            Split, 12

 

      15   Set(x+y) & Set(x)

            Join, 13, 6

 

      16   x+y<=x <=> ALL(c):[c e x+y => c e x]

            Detach, 9, 15

 

      17   [x+y<=x => ALL(c):[c e x+y => c e x]]

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

            Iff-And, 16

 

      18   x+y<=x => ALL(c):[c e x+y => c e x]

            Split, 17

 

    Sufficient: For x+y<=x

 

      19   ALL(c):[c e x+y => c e x] => x+y<=x

            Split, 17

 

        

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

        

         Suppose...

 

            20   z e x+y

                  Premise

 

         From definition of x+y...

 

            21   z e x+y <=> z e x & z e y

                  U Spec, 14

 

            22   [z e x+y => z e x & z e y] & [z e x & z e y => z e x+y]

                  Iff-And, 21

 

            23   z e x+y => z e x & z e y

                  Split, 22

 

            24   z e x & z e y => z e x+y

                  Split, 22

 

            25   z e x & z e y

                  Detach, 23, 20

 

            26   z e x

                  Split, 25

 

    As Required:

 

      27   ALL(c):[c e x+y => c e x]

            4 Conclusion, 20

 

      28   x+y<=x

            Detach, 19, 27

 

As Required:

 

29   ALL(a):ALL(b):[Set(a) & Set(b) => a+b<=a]

      4 Conclusion, 5