THEOREM
*******
On every set s1 there exists a complement function mapping every subset of s1 to its complement wrt s1.
ALL(s1):ALL(ps1):[Set(s1) & Set(ps1)
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
=> EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]
& ALL(a):[a e ps1 => ALL(b):[b e s1 => [b e f1(a) <=> ~b e a]]]]]
PROOF
*****
Suppose...
1 Set(x) & Set(px)
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
Premise
2 Set(x)
Split, 1
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
Apply Cartesian Product Axiom
5 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
6 ALL(a2):[Set(px) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e a2]]]
U Spec, 5
7 Set(px) & Set(px) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]
U Spec, 6
8 Set(px) & Set(px)
Join, 3, 3
9 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]
Detach, 7, 8
10 Set'(px2) & ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]
E Spec, 9
Define: px2 (the Cartesian product of px)
***********
11 Set'(px2)
Split, 10
12 ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]
Split, 10
Apply Subset Axiom
13 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e a]]]]
Subset, 11
14 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
15 Set'(cx) & ALL(a):ALL(b):[(a,b) e cx <=> (a,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e a]]]
E Spec, 13
Define: cx (a subset of px2)
**********
16 Set'(cx)
Split, 15
17 ALL(a):ALL(b):[(a,b) e cx <=> (a,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e a]]]
Split, 15
Prove: cx is a function mapping px to itself
Apply Function Axiom
18 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
19 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e cx => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e cx]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
=> ALL(c):ALL(d):[d=cx(c) <=> (c,d) e cx]]
U Spec, 18
20 ALL(b):[ALL(c):ALL(d):[(c,d) e cx => c e px & d e b]
& ALL(c):[c e px => EXIST(d):[d e b & (c,d) e cx]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
=> ALL(c):ALL(d):[d=cx(c) <=> (c,d) e cx]]
U Spec, 19
Sufficient: For functionality of cx
21 ALL(c):ALL(d):[(c,d) e cx => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px & (c,d) e cx]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
=> ALL(c):ALL(d):[d=cx(c) <=> (c,d) e cx]
U Spec, 20
Prove: ALL(c):ALL(d):[(c,d) e cx => c e px & d e px]
Suppose...
22 (p,q) e cx
Premise
23 ALL(b):[(p,b) e cx <=> (p,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e p]]]
U Spec, 17
24 (p,q) e cx <=> (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
U Spec, 23
25 [(p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]]
& [(p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx]
Iff-And, 24
26 (p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
Split, 25
27 (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx
Split, 25
28 (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
Detach, 26, 22
29 (p,q) e px2
Split, 28
30 ALL(c):[c e x => [c e q <=> ~c e p]]
Split, 28
31 ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]
U Spec, 12
Apply definition of px2
32 (p,q) e px2 <=> p e px & q e px
U Spec, 31
33 [(p,q) e px2 => p e px & q e px]
& [p e px & q e px => (p,q) e px2]
Iff-And, 32
34 (p,q) e px2 => p e px & q e px
Split, 33
35 p e px & q e px => (p,q) e px2
Split, 33
36 p e px & q e px
Detach, 34, 29
As Required:
37 ALL(c):ALL(d):[(c,d) e cx => c e px & d e px]
4 Conclusion, 22
Prove: ALL(c):[c e px => EXIST(d):[d e px & (c,d) e cx]]
Suppose...
38 p e px
Premise
Apply Subset Axiom
39 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & ~a e p]]
Subset, 2
40 Set(q) & ALL(a):[a e q <=> a e x & ~a e p]
E Spec, 39
Define: q (the complement of p wrt x)
*********
41 Set(q)
Split, 40
42 ALL(a):[a e q <=> a e x & ~a e p]
Split, 40
Apply the definition of cx
43 ALL(b):[(p,b) e cx <=> (p,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e p]]]
U Spec, 17
44 (p,q) e cx <=> (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
U Spec, 43
45 [(p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]]
& [(p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx]
Iff-And, 44
46 (p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
Split, 45
47 (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx
Split, 45
Apply the definition of px2
48 ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]
U Spec, 12
49 (p,q) e px2 <=> p e px & q e px
U Spec, 48
50 [(p,q) e px2 => p e px & q e px]
& [p e px & q e px => (p,q) e px2]
Iff-And, 49
51 (p,q) e px2 => p e px & q e px
Split, 50
52 p e px & q e px => (p,q) e px2
Split, 50
53 q e px <=> Set(q) & ALL(b):[b e q => b e x]
U Spec, 4
54 [q e px => Set(q) & ALL(b):[b e q => b e x]]
& [Set(q) & ALL(b):[b e q => b e x] => q e px]
Iff-And, 53
55 q e px => Set(q) & ALL(b):[b e q => b e x]
Split, 54
56 Set(q) & ALL(b):[b e q => b e x] => q e px
Split, 54
Prove: ALL(c):[c e q => c e x]
Suppose...
57 r e q
Premise
58 r e q <=> r e x & ~r e p
U Spec, 42
59 [r e q => r e x & ~r e p] & [r e x & ~r e p => r e q]
Iff-And, 58
60 r e q => r e x & ~r e p
Split, 59
61 r e x & ~r e p => r e q
Split, 59
62 r e x & ~r e p
Detach, 60, 57
63 r e x
Split, 62
As Required:
64 ALL(c):[c e q => c e x]
4 Conclusion, 57
65 Set(q) & ALL(c):[c e q => c e x]
Join, 41, 64
66 q e px
Detach, 56, 65
67 p e px & q e px
Join, 38, 66
68 (p,q) e px2
Detach, 52, 67
Prove: ALL(c):[c e x => [c e q <=> ~c e p]]
Suppose...
69 r e x
Premise
Prove: r e q => ~r e p
Suppose...
70 r e q
Premise
71 r e q <=> r e x & ~r e p
U Spec, 42
72 [r e q => r e x & ~r e p] & [r e x & ~r e p => r e q]
Iff-And, 71
73 r e q => r e x & ~r e p
Split, 72
74 r e x & ~r e p => r e q
Split, 72
75 r e x & ~r e p
Detach, 73, 70
76 r e x
Split, 75
77 ~r e p
Split, 75
As Required:
78 r e q => ~r e p
4 Conclusion, 70
Prove: ~r e p => r e q
Suppose...
79 ~r e p
Premise
80 r e q <=> r e x & ~r e p
U Spec, 42
81 [r e q => r e x & ~r e p] & [r e x & ~r e p => r e q]
Iff-And, 80
82 r e q => r e x & ~r e p
Split, 81
83 r e x & ~r e p => r e q
Split, 81
84 r e x & ~r e p
Join, 69, 79
85 r e q
Detach, 83, 84
As Required:
86 ~r e p => r e q
4 Conclusion, 79
87 [r e q => ~r e p] & [~r e p => r e q]
Join, 78, 86
88 r e q <=> ~r e p
Iff-And, 87
As Required:
89 ALL(c):[c e x => [c e q <=> ~c e p]]
4 Conclusion, 69
90 (p,q) e px2
& ALL(c):[c e x => [c e q <=> ~c e p]]
Join, 68, 89
91 (p,q) e cx
Detach, 47, 90
92 q e px & (p,q) e cx
Join, 66, 91
As Required:
93 ALL(c):[c e px => EXIST(d):[d e px & (c,d) e cx]]
4 Conclusion, 38
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
Suppose...
94 (p,q1) e cx & (p,q2) e cx
Premise
95 (p,q1) e cx
Split, 94
96 (p,q2) e cx
Split, 94
Apply Set Equality Axiom
97 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
98 ALL(b):[Set(q1) & Set(b) => [q1=b <=> ALL(c):[c e q1 <=> c e b]]]
U Spec, 97
99 Set(q1) & Set(q2) => [q1=q2 <=> ALL(c):[c e q1 <=> c e q2]]
U Spec, 98
Apply the definition of cx
100 ALL(b):[(p,b) e cx <=> (p,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e p]]]
U Spec, 17
101 (p,q1) e cx <=> (p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]]
U Spec, 100
102 [(p,q1) e cx => (p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]]]
& [(p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]] => (p,q1) e cx]
Iff-And, 101
103 (p,q1) e cx => (p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]]
Split, 102
104 (p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]] => (p,q1) e cx
Split, 102
105 (p,q1) e px2 & ALL(c):[c e x => [c e q1 <=> ~c e p]]
Detach, 103, 95
106 (p,q1) e px2
Split, 105
107 ALL(c):[c e x => [c e q1 <=> ~c e p]]
Split, 105
108 ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]
U Spec, 12
109 (p,q1) e px2 <=> p e px & q1 e px
U Spec, 108
110 [(p,q1) e px2 => p e px & q1 e px]
& [p e px & q1 e px => (p,q1) e px2]
Iff-And, 109
111 (p,q1) e px2 => p e px & q1 e px
Split, 110
112 p e px & q1 e px => (p,q1) e px2
Split, 110
113 p e px & q1 e px
Detach, 111, 106
114 p e px
Split, 113
115 q1 e px
Split, 113
116 q1 e px <=> Set(q1) & ALL(b):[b e q1 => b e x]
U Spec, 4
117 [q1 e px => Set(q1) & ALL(b):[b e q1 => b e x]]
& [Set(q1) & ALL(b):[b e q1 => b e x] => q1 e px]
Iff-And, 116
118 q1 e px => Set(q1) & ALL(b):[b e q1 => b e x]
Split, 117
119 Set(q1) & ALL(b):[b e q1 => b e x] => q1 e px
Split, 117
120 Set(q1) & ALL(b):[b e q1 => b e x]
Detach, 118, 115
121 Set(q1)
Split, 120
122 ALL(b):[b e q1 => b e x]
Split, 120
123 (p,q2) e cx <=> (p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]]
U Spec, 100
124 [(p,q2) e cx => (p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]]]
& [(p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]] => (p,q2) e cx]
Iff-And, 123
125 (p,q2) e cx => (p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]]
Split, 124
126 (p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]] => (p,q2) e cx
Split, 124
127 (p,q2) e px2 & ALL(c):[c e x => [c e q2 <=> ~c e p]]
Detach, 125, 96
128 (p,q2) e px2
Split, 127
129 ALL(c):[c e x => [c e q2 <=> ~c e p]]
Split, 127
130 (p,q2) e px2 <=> p e px & q2 e px
U Spec, 108
131 [(p,q2) e px2 => p e px & q2 e px]
& [p e px & q2 e px => (p,q2) e px2]
Iff-And, 130
132 (p,q2) e px2 => p e px & q2 e px
Split, 131
133 p e px & q2 e px => (p,q2) e px2
Split, 131
134 p e px & q2 e px
Detach, 132, 128
135 p e px
Split, 134
136 q2 e px
Split, 134
137 q2 e px <=> Set(q2) & ALL(b):[b e q2 => b e x]
U Spec, 4
138 [q2 e px => Set(q2) & ALL(b):[b e q2 => b e x]]
& [Set(q2) & ALL(b):[b e q2 => b e x] => q2 e px]
Iff-And, 137
139 q2 e px => Set(q2) & ALL(b):[b e q2 => b e x]
Split, 138
140 Set(q2) & ALL(b):[b e q2 => b e x] => q2 e px
Split, 138
141 Set(q2) & ALL(b):[b e q2 => b e x]
Detach, 139, 136
142 Set(q2)
Split, 141
143 ALL(b):[b e q2 => b e x]
Split, 141
144 Set(q1) & Set(q2)
Join, 121, 142
145 q1=q2 <=> ALL(c):[c e q1 <=> c e q2]
Detach, 99, 144
146 [q1=q2 => ALL(c):[c e q1 <=> c e q2]]
& [ALL(c):[c e q1 <=> c e q2] => q1=q2]
Iff-And, 145
147 q1=q2 => ALL(c):[c e q1 <=> c e q2]
Split, 146
148 ALL(c):[c e q1 <=> c e q2] => q1=q2
Split, 146
Prove: ALL(c):[c e q1 => c e q2]
Suppose...
149 r e q1
Premise
150 r e x => [r e q1 <=> ~r e p]
U Spec, 107
151 r e q1 => r e x
U Spec, 122
152 r e x
Detach, 151, 149
153 r e q1 <=> ~r e p
Detach, 150, 152
154 [r e q1 => ~r e p] & [~r e p => r e q1]
Iff-And, 153
155 r e q1 => ~r e p
Split, 154
156 ~r e p => r e q1
Split, 154
157 ~r e p
Detach, 155, 149
158 r e x => [r e q2 <=> ~r e p]
U Spec, 129
159 r e q2 <=> ~r e p
Detach, 158, 152
160 [r e q2 => ~r e p] & [~r e p => r e q2]
Iff-And, 159
161 r e q2 => ~r e p
Split, 160
162 ~r e p => r e q2
Split, 160
163 r e q2
Detach, 162, 157
As Required:
164 ALL(c):[c e q1 => c e q2]
4 Conclusion, 149
Prove: ALL(c):[c e q2 => c e q1]
Suppose...
165 r e q2
Premise
166 r e x => [r e q2 <=> ~r e p]
U Spec, 129
Apply the definition of px
167 q2 e px <=> Set(q2) & ALL(b):[b e q2 => b e x]
U Spec, 4
168 [q2 e px => Set(q2) & ALL(b):[b e q2 => b e x]]
& [Set(q2) & ALL(b):[b e q2 => b e x] => q2 e px]
Iff-And, 167
169 q2 e px => Set(q2) & ALL(b):[b e q2 => b e x]
Split, 168
170 Set(q2) & ALL(b):[b e q2 => b e x] => q2 e px
Split, 168
171 Set(q2) & ALL(b):[b e q2 => b e x]
Detach, 169, 136
172 Set(q2)
Split, 171
173 ALL(b):[b e q2 => b e x]
Split, 171
174 r e q2 => r e x
U Spec, 173
175 r e x
Detach, 174, 165
176 r e q2 <=> ~r e p
Detach, 166, 175
177 [r e q2 => ~r e p] & [~r e p => r e q2]
Iff-And, 176
178 r e q2 => ~r e p
Split, 177
179 ~r e p => r e q2
Split, 177
180 ~r e p
Detach, 178, 165
181 r e x => [r e q1 <=> ~r e p]
U Spec, 107
182 r e q1 <=> ~r e p
Detach, 181, 175
183 [r e q1 => ~r e p] & [~r e p => r e q1]
Iff-And, 182
184 r e q1 => ~r e p
Split, 183
185 ~r e p => r e q1
Split, 183
186 r e q1
Detach, 185, 180
As Required:
187 ALL(c):[c e q2 => c e q1]
4 Conclusion, 165
188 ALL(c):[[c e q1 => c e q2] & [c e q2 => c e q1]]
Join, 164, 187
189 ALL(c):[c e q1 <=> c e q2]
Iff-And, 188
190 q1=q2
Detach, 148, 189
As Required:
191 ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
4 Conclusion, 94
192 ALL(c):ALL(d):[(c,d) e cx => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px & (c,d) e cx]]
Join, 37, 93
193 ALL(c):ALL(d):[(c,d) e cx => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px & (c,d) e cx]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e cx & (c,d2) e cx => d1=d2]
Join, 192, 191
As Required: cx is a function
194 ALL(c):ALL(d):[d=cx(c) <=> (c,d) e cx]
Detach, 21, 193
Prove: ALL(a):[a e px => cx(a) e px]
Suppose...
195 p e px
Premise
196 p e px => EXIST(d):[d e px & (p,d) e cx]
U Spec, 93
197 EXIST(d):[d e px & (p,d) e cx]
Detach, 196, 195
198 q e px & (p,q) e cx
E Spec, 197
199 q e px
Split, 198
200 (p,q) e cx
Split, 198
201 ALL(d):[d=cx(p) <=> (p,d) e cx]
U Spec, 194
202 q=cx(p) <=> (p,q) e cx
U Spec, 201
203 [q=cx(p) => (p,q) e cx] & [(p,q) e cx => q=cx(p)]
Iff-And, 202
204 q=cx(p) => (p,q) e cx
Split, 203
205 (p,q) e cx => q=cx(p)
Split, 203
206 q=cx(p)
Detach, 205, 200
207 cx(p) e px
Substitute, 206, 199
As Required:
208 ALL(a):[a e px => cx(a) e px]
4 Conclusion, 195
Prove: ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
Suppose...
209 p e px
Premise
210 p e px => EXIST(d):[d e px & (p,d) e cx]
U Spec, 93
211 EXIST(d):[d e px & (p,d) e cx]
Detach, 210, 209
212 q e px & (p,q) e cx
E Spec, 211
213 q e px
Split, 212
214 (p,q) e cx
Split, 212
215 ALL(b):[(p,b) e cx <=> (p,b) e px2 & ALL(c):[c e x => [c e b <=> ~c e p]]]
U Spec, 17
216 (p,q) e cx <=> (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
U Spec, 215
217 [(p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]]
& [(p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx]
Iff-And, 216
218 (p,q) e cx => (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
Split, 217
219 (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]] => (p,q) e cx
Split, 217
220 (p,q) e px2 & ALL(c):[c e x => [c e q <=> ~c e p]]
Detach, 218, 214
221 (p,q) e px2
Split, 220
222 ALL(c):[c e x => [c e q <=> ~c e p]]
Split, 220
223 ALL(d):[d=cx(p) <=> (p,d) e cx]
U Spec, 194
224 q=cx(p) <=> (p,q) e cx
U Spec, 223
225 [q=cx(p) => (p,q) e cx] & [(p,q) e cx => q=cx(p)]
Iff-And, 224
226 q=cx(p) => (p,q) e cx
Split, 225
227 (p,q) e cx => q=cx(p)
Split, 225
228 q=cx(p)
Detach, 227, 214
229 ALL(c):[c e x => [c e cx(p) <=> ~c e p]]
Substitute, 228, 222
As Required:
230 ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
4 Conclusion, 209
231 ALL(a):[a e px => cx(a) e px]
& ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
Join, 208, 230
As Required:
232 ALL(s1):ALL(ps1):[Set(s1) & Set(ps1)
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
=> EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]
& ALL(a):[a e ps1 => ALL(c):[c e s1 => [c e f1(a) <=> ~c e a]]]]]
4 Conclusion, 1