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