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