THEOREM
*******
The complement of the complement of set x is x itself.
ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e s]]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):[a e ps => ALL(b):[b e s => [b e f(a) <=> ~b e a]]]
=> ALL(a):[a e ps => f(f(a))=a]]
PROOF
*****
Suppose...
1 Set(x)
& Set(px)
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e px => cx(a) e px]
& ALL(a):[a e px => ALL(b):[b e x => [b e cx(a) <=> ~b e a]]]
Premise
2 Set(x)
Split, 1
Define: px
**********
3 Set(px)
Split, 1
px is the power set of x
4 ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
Split, 1
Define: cx (the complement wrt x)
**********
5 ALL(a):[a e px => cx(a) e px]
Split, 1
6 ALL(a):[a e px => ALL(b):[b e x => [b e cx(a) <=> ~b e a]]]
Split, 1
Prove: ALL(a):[aepx => [cx(cx(a))=a]]
Suppose...
7 p e px
Premise
Apply Set Equality Axioms
8 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
9 ALL(b):[Set(cx(cx(p))) & Set(b) => [cx(cx(p))=b <=> ALL(c):[c e cx(cx(p)) <=> c e b]]]
U Spec, 8
10 Set(cx(cx(p))) & Set(p) => [cx(cx(p))=p <=> ALL(c):[c e cx(cx(p)) <=> c e p]]
U Spec, 9
Prove: Set(cx(cx(p)))
Apply definition of px(p)
11 p e px => cx(p) e px
U Spec, 5
12 cx(p) e px
Detach, 11, 7
Apply definition of cx(cx(p))
13 cx(p) e px => cx(cx(p)) e px
U Spec, 5
14 cx(cx(p)) e px
Detach, 13, 12
15 cx(cx(p)) e px <=> Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
U Spec, 4
16 [cx(cx(p)) e px => Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]]
& [Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x] => cx(cx(p)) e px]
Iff-And, 15
17 cx(cx(p)) e px => Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
Split, 16
18 Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x] => cx(cx(p)) e px
Split, 16
19 Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
Detach, 17, 14
As Required:
20 Set(cx(cx(p)))
Split, 19
Prove: Set(p)
Apply definition of cx(cx(p))
21 ALL(b):[b e cx(cx(p)) => b e x]
Split, 19
22 p e px <=> Set(p) & ALL(b):[b e p => b e x]
U Spec, 4
23 [p e px => Set(p) & ALL(b):[b e p => b e x]]
& [Set(p) & ALL(b):[b e p => b e x] => p e px]
Iff-And, 22
24 p e px => Set(p) & ALL(b):[b e p => b e x]
Split, 23
25 Set(p) & ALL(b):[b e p => b e x] => p e px
Split, 23
26 Set(p) & ALL(b):[b e p => b e x]
Detach, 24, 7
As Required:
27 Set(p)
Split, 26
28 ALL(b):[b e p => b e x]
Split, 26
29 Set(cx(cx(p))) & Set(p)
Join, 20, 27
30 cx(cx(p))=p <=> ALL(c):[c e cx(cx(p)) <=> c e p]
Detach, 10, 29
31 [cx(cx(p))=p => ALL(c):[c e cx(cx(p)) <=> c e p]]
& [ALL(c):[c e cx(cx(p)) <=> c e p] => cx(cx(p))=p]
Iff-And, 30
32 cx(cx(p))=p => ALL(c):[c e cx(cx(p)) <=> c e p]
Split, 31
Sufficient: For cx(cx(p))=p
33 ALL(c):[c e cx(cx(p)) <=> c e p] => cx(cx(p))=p
Split, 31
'=>'
Prove: ALL(c):[c e cx(cx(p)) => c e p]
Suppose...
34 q e cx(cx(p))
Premise
Apply definition of cx for p
35 p e px => ALL(b):[b e x => [b e cx(p) <=> ~b e p]]
U Spec, 6
36 ALL(b):[b e x => [b e cx(p) <=> ~b e p]]
Detach, 35, 7
Apply definition of cx for cx(p)
37 cx(p) e px => ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
U Spec, 6
38 ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
Detach, 37, 12
Prove: q e p
Suppose to contrary...
39 ~q e p
Premise
From definition of cx for cx(p)
40 q e x => [q e cx(p) <=> ~q e p]
U Spec, 36
Apply definition of px
41 cx(cx(p)) e px <=> Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
U Spec, 4
42 [cx(cx(p)) e px => Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]]
& [Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x] => cx(cx(p)) e px]
Iff-And, 41
43 cx(cx(p)) e px => Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
Split, 42
44 Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x] => cx(cx(p)) e px
Split, 42
45 Set(cx(cx(p))) & ALL(b):[b e cx(cx(p)) => b e x]
Detach, 43, 14
46 Set(cx(cx(p)))
Split, 45
Apply definition of cx(cx(p))
47 ALL(b):[b e cx(cx(p)) => b e x]
Split, 45
48 q e cx(cx(p)) => q e x
U Spec, 47
49 q e x
Detach, 48, 34
50 q e cx(p) <=> ~q e p
Detach, 40, 49
51 [q e cx(p) => ~q e p] & [~q e p => q e cx(p)]
Iff-And, 50
52 q e cx(p) => ~q e p
Split, 51
53 ~q e p => q e cx(p)
Split, 51
54 q e cx(p)
Detach, 53, 39
Apply definition of cx(cx(p)) (repeated)
55 cx(p) e px => ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
U Spec, 6
56 ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
Detach, 55, 12
57 q e x => [q e cx(cx(p)) <=> ~q e cx(p)]
U Spec, 56
58 q e cx(cx(p)) <=> ~q e cx(p)
Detach, 57, 49
59 [q e cx(cx(p)) => ~q e cx(p)]
& [~q e cx(p) => q e cx(cx(p))]
Iff-And, 58
60 q e cx(cx(p)) => ~q e cx(p)
Split, 59
61 ~q e cx(p) => q e cx(cx(p))
Split, 59
62 ~q e cx(p)
Detach, 60, 34
Obtain the contradiction...
63 q e cx(p) & ~q e cx(p)
Join, 54, 62
As Required:
64 ~~q e p
4 Conclusion, 39
65 q e p
Rem DNeg, 64
'=>'
As Required:
66 ALL(c):[c e cx(cx(p)) => c e p]
4 Conclusion, 34
'<='
Prove: ALL(c):[c e p => c e cx(cx(p))]
Suppose...
67 q e p
Premise
Apply definition of cx(p)
68 p e px => ALL(b):[b e x => [b e cx(p) <=> ~b e p]]
U Spec, 6
69 ALL(b):[b e x => [b e cx(p) <=> ~b e p]]
Detach, 68, 7
70 q e x => [q e cx(p) <=> ~q e p]
U Spec, 69
71 q e p => q e x
U Spec, 28
72 q e x
Detach, 71, 67
73 q e cx(p) <=> ~q e p
Detach, 70, 72
74 [q e cx(p) => ~q e p] & [~q e p => q e cx(p)]
Iff-And, 73
75 q e cx(p) => ~q e p
Split, 74
76 ~q e p => q e cx(p)
Split, 74
77 ~~q e p => ~q e cx(p)
Contra, 75
78 q e p => ~q e cx(p)
Rem DNeg, 77
79 ~q e cx(p)
Detach, 78, 67
Prove: q e cx(cx(p))
Suppose to the contrary...
80 ~q e cx(cx(p))
Premise
Apply definition of cx(cx(p))
81 cx(p) e px => ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
U Spec, 6
82 ALL(b):[b e x => [b e cx(cx(p)) <=> ~b e cx(p)]]
Detach, 81, 12
83 q e x => [q e cx(cx(p)) <=> ~q e cx(p)]
U Spec, 82
84 q e cx(cx(p)) <=> ~q e cx(p)
Detach, 83, 72
85 [q e cx(cx(p)) => ~q e cx(p)]
& [~q e cx(p) => q e cx(cx(p))]
Iff-And, 84
86 q e cx(cx(p)) => ~q e cx(p)
Split, 85
87 ~q e cx(p) => q e cx(cx(p))
Split, 85
88 ~q e cx(cx(p)) => ~~q e cx(p)
Contra, 87
89 ~q e cx(cx(p)) => q e cx(p)
Rem DNeg, 88
90 q e cx(p)
Detach, 89, 80
91 q e cx(p) & ~q e cx(p)
Join, 90, 79
As Required:
92 ~~q e cx(cx(p))
4 Conclusion, 80
93 q e cx(cx(p))
Rem DNeg, 92
'<='
As Required:
94 ALL(c):[c e p => c e cx(cx(p))]
4 Conclusion, 67
95 ALL(c):[[c e cx(cx(p)) => c e p] & [c e p => c e cx(cx(p))]]
Join, 66, 94
96 ALL(c):[c e cx(cx(p)) <=> c e p]
Iff-And, 95
97 cx(cx(p))=p
Detach, 33, 96
As Required:
98 ALL(a):[a e px => cx(cx(a))=a]
4 Conclusion, 7
As Required:
99 ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e s]]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):[a e ps => ALL(b):[b e s => [b e f(a) <=> ~b e a]]]
=> ALL(a):[a e ps => f(f(a))=a]]
4 Conclusion, 1