Suppose...
1 ALL(a):[a e x => a e u]
& ALL(a):[a e y => a e u]
& ALL(a):[a e x' <=> a e u & ~a e x]
& ALL(a):[a e y' <=> a e u & ~a e y]
Premise
x is a subset of u
2 ALL(a):[a e x => a e u]
Split, 1
y is a subset of u
3 ALL(a):[a e y => a e u]
Split, 1
x' is the complement of x wrt u
4 ALL(a):[a e x' <=> a e u & ~a e x]
Split, 1
y' is the complement of y wrt u
5 ALL(a):[a e y' <=> a e u & ~a e y]
Split, 1
'=>'
Prove: ALL(a):[a e x => a e y] => ALL(a):[a e y' => a e x']
Suppose...
6 ALL(a):[a e x => a e y]
Premise
Prove: ALL(a):[a e y' => a e x']
Suppose...
7 p e y'
Premise
Apply definition of y'
8 p e y' <=> p e u & ~p e y
U Spec, 5
Apply Iff-And Rule
9 [p e y' => p e u & ~p e y] & [p e u & ~p e y => p e y']
Iff-And, 8
10 p e y' => p e u & ~p e y
Split, 9
11 p e u & ~p e y => p e y'
Split, 9
Apply Detachment Rule
12 p e u & ~p e y
Detach, 10, 7
13 p e u
Split, 12
14 ~p e y
Split, 12
Apply definition of x'
15 p e x' <=> p e u & ~p e x
U Spec, 4
Apply Iff-And Rule
16 [p e x' => p e u & ~p e x] & [p e u & ~p e x => p e x']
Iff-And, 15
17 p e x' => p e u & ~p e x
Split, 16
Sufficient: For p e x'
18 p e u & ~p e x => p e x'
Split, 16
Apply premise
19 p e x => p e y
U Spec, 6
Apply Contrapostive Rule
20 ~p e y => ~p e x
Contra, 19
Apply Detachment Rule
21 ~p e x
Detach, 20, 14
22 p e u & ~p e x
Join, 13, 21
Apply Detachment Rule
23 p e x'
Detach, 18, 22
As Required:
24 ALL(a):[a e y' => a e x']
4 Conclusion, 7
'=>'
As Required:
25 ALL(a):[a e x => a e y] => ALL(a):[a e y' => a e x']
4 Conclusion, 6
'<='
Prove: ALL(a):[a e y' => a e x'] => ALL(a):[a e x => a e y]
Suppose...
26 ALL(a):[a e y' => a e x']
Premise
Prove: ALL(a):[a e x => a e y]
Suppose...
27 p e x
Premise
Apply definition of x'
28 p e x' <=> p e u & ~p e x
U Spec, 4
Apply Iff-And Rule
29 [p e x' => p e u & ~p e x] & [p e u & ~p e x => p e x']
Iff-And, 28
30 p e x' => p e u & ~p e x
Split, 29
31 p e u & ~p e x => p e x'
Split, 29
Apply Contrapositive Rule
32 ~[p e u & ~p e x] => ~p e x'
Contra, 30
Apply DeMorgan Rule
33 ~~[~p e u | ~~p e x] => ~p e x'
DeMorgan, 32
Remove '~~'
34 ~p e u | ~~p e x => ~p e x'
Rem DNeg, 33
35 ~p e u | p e x => ~p e x'
Rem DNeg, 34
Apply Arbitrary-Or Rule
36 ~p e u | p e x
Arb Or, 27
Apply Detachment Rule
37 ~p e x'
Detach, 35, 36
Apply definition of y'
38 p e y' <=> p e u & ~p e y
U Spec, 5
Apply Iff-And Rule
39 [p e y' => p e u & ~p e y] & [p e u & ~p e y => p e y']
Iff-And, 38
40 p e y' => p e u & ~p e y
Split, 39
41 p e u & ~p e y => p e y'
Split, 39
Apply premise
42 p e y' => p e x'
U Spec, 26
Apply Contrapositive Rule
43 ~p e x' => ~p e y'
Contra, 42
Apply Detachment Rule
44 ~p e y'
Detach, 43, 37
Apply Contrapositive Rule
45 ~p e y' => ~[p e u & ~p e y]
Contra, 41
Apply Detachment Rule
46 ~[p e u & ~p e y]
Detach, 45, 44
Apply Imply-And Rule
47 ~~[p e u => ~~p e y]
Imply-And, 46
Remove '~~'
48 p e u => ~~p e y
Rem DNeg, 47
49 p e u => p e y
Rem DNeg, 48
Apply definition of x
50 p e x => p e u
U Spec, 2
Apply Detachment Rule
51 p e u
Detach, 50, 27
52 p e y
Detach, 49, 51
As Required:
53 ALL(a):[a e x => a e y]
4 Conclusion, 27
'<='
As Required:
54 ALL(a):[a e y' => a e x'] => ALL(a):[a e x => a e y]
4 Conclusion, 26
55 [ALL(a):[a e x => a e y] => ALL(a):[a e y' => a e x']]
& [ALL(a):[a e y' => a e x'] => ALL(a):[a e x => a e y]]
Join, 25, 54
As Required:
56 ALL(a):[a e x => a e y] <=> ALL(a):[a e y' => a e x']
Iff-And, 55