THEOREM
*******
ALL(s):[Set(s) => EXIST(a):EXIST(b):[Set(a) & Set(b) & a e b & ~ALL(c):[c e a => c e b]]]
Note: This proof was written and mechanically verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
PROOF
*****
Suppose...
1 Set(s)
Premise
Construct null
Apply Subset Axiom
2 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]
Subset, 1
3 Set(null) & ALL(a):[a e null <=> a e s & ~a e s]
E Spec, 2
Define: Null
************
4 Set(null)
Split, 3
5 ALL(a):[a e null <=> a e s & ~a e s]
Split, 3
Prove: ~EXIST(a):a e null
Suppose to the contrary...
6 x e null
Premise
Apply definition of null
7 x e null <=> x e s & ~x e s
U Spec, 5
8 [x e null => x e s & ~x e s]
& [x e s & ~x e s => x e null]
Iff-And, 7
9 x e null => x e s & ~x e s
Split, 8
10 x e s & ~x e s => x e null
Split, 8
11 x e s & ~x e s
Detach, 9, 6
As Required:
12 ~EXIST(a):a e null
4 Conclusion, 6
13 ~~ALL(a):~a e null
Quant, 12
As Required:
14 ALL(a):~a e null
Rem DNeg, 13
Construct ps
Apply Power Set Axiom
15 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]
Power Set
16 Set(s) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e s]]]
U Spec, 15
17 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e s]]]
Detach, 16, 1
18 Set(ps)
& ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
E Spec, 17
Define: ps (power set of s)
**********
19 Set(ps)
Split, 18
20 ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
Split, 18
Construct t
Apply Subset Axiom
21 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e ps & a=null]]
Subset, 19
22 Set(t) & ALL(a):[a e t <=> a e ps & a=null]
E Spec, 21
Define: t
*********
23 Set(t)
Split, 22
24 ALL(a):[a e t <=> a e ps & a=null]
Split, 22
Prove: ALL(a):[a e t <=> a=null]
'=>'
Suppose...
25 x e t
Premise
Apply definition of t
26 x e t <=> x e ps & x=null
U Spec, 24
27 [x e t => x e ps & x=null] & [x e ps & x=null => x e t]
Iff-And, 26
28 x e t => x e ps & x=null
Split, 27
29 x e ps & x=null => x e t
Split, 27
30 x e ps & x=null
Detach, 28, 25
31 x e ps
Split, 30
32 x=null
Split, 30
As Required:
33 ALL(a):[a e t => a=null]
4 Conclusion, 25
'<='
Suppose...
34 x=null
Premise
Prove: x e t
Apply definition of t
35 x e t <=> x e ps & x=null
U Spec, 24
36 [x e t => x e ps & x=null] & [x e ps & x=null => x e t]
Iff-And, 35
37 x e t => x e ps & x=null
Split, 36
Sufficient: For x e t
38 x e ps & x=null => x e t
Split, 36
Prove: x e ps
Apply definition of ps
39 x e ps <=> Set(x) & ALL(d):[d e x => d e s]
U Spec, 20
40 [x e ps => Set(x) & ALL(d):[d e x => d e s]]
& [Set(x) & ALL(d):[d e x => d e s] => x e ps]
Iff-And, 39
41 x e ps => Set(x) & ALL(d):[d e x => d e s]
Split, 40
Sufficient: For x e ps
42 Set(x) & ALL(d):[d e x => d e s] => x e ps
Split, 40
43 Set(x)
Substitute, 34, 4
Prove: ALL(d):[d e x => d e s]
Suppose...
44 y e x
Premise
45 y e null
Substitute, 34, 44
Apply definition of null
46 ~y e null
U Spec, 14
47 ~~y e null => y e s
Arb Cons, 46
48 y e null => y e s
Rem DNeg, 47
49 y e s
Detach, 48, 45
As Required:
50 ALL(d):[d e x => d e s]
4 Conclusion, 44
Joining results
51 Set(x) & ALL(d):[d e x => d e s]
Join, 43, 50
As Required:
52 x e ps
Detach, 42, 51
Join results
53 x e ps & x=null
Join, 52, 34
54 x e t
Detach, 38, 53
As Required:
55 ALL(a):[a=null => a e t]
4 Conclusion, 34
Join results
56 ALL(a):[[a e t => a=null] & [a=null => a e t]]
Join, 33, 55
As Required:
57 ALL(a):[a e t <=> a=null]
Iff-And, 56
Construct pps
Apply Power Set Axiom
58 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]
Power Set
59 Set(ps) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e ps]]]
U Spec, 58
60 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e ps]]]
Detach, 59, 19
61 Set(pps)
& ALL(c):[c e pps <=> Set(c) & ALL(d):[d e c => d e ps]]
E Spec, 60
Define: pps (the power set of ps)
***********
62 Set(pps)
Split, 61
63 ALL(c):[c e pps <=> Set(c) & ALL(d):[d e c => d e ps]]
Split, 61
Construct u
Apply Subset Axiom
64 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pps & a=t]]
Subset, 62
65 Set(u) & ALL(a):[a e u <=> a e pps & a=t]
E Spec, 64
Define: u
*********
66 Set(u)
Split, 65
67 ALL(a):[a e u <=> a e pps & a=t]
Split, 65
Prove: ALL(a):[a e u => a=t]
Suppose...
68 x e u
Premise
Prove: x=t
Apply definition of u
69 x e u <=> x e pps & x=t
U Spec, 67
70 [x e u => x e pps & x=t] & [x e pps & x=t => x e u]
Iff-And, 69
71 x e u => x e pps & x=t
Split, 70
72 x e pps & x=t => x e u
Split, 70
73 x e pps & x=t
Detach, 71, 68
74 x e pps
Split, 73
As Required:
75 x=t
Split, 73
As Required:
76 ALL(a):[a e u => a=t]
4 Conclusion, 68
Prove: ALL(a):[a=t => a e u]
Suppose...
77 x=t
Premise
Prove: x e u
Apply definition of u
78 x e u <=> x e pps & x=t
U Spec, 67
79 [x e u => x e pps & x=t] & [x e pps & x=t => x e u]
Iff-And, 78
80 x e u => x e pps & x=t
Split, 79
Sufficient: For x e u
81 x e pps & x=t => x e u
Split, 79
Prove: x e pps
Apply definition of pps
82 x e pps <=> Set(x) & ALL(d):[d e x => d e ps]
U Spec, 63
83 [x e pps => Set(x) & ALL(d):[d e x => d e ps]]
& [Set(x) & ALL(d):[d e x => d e ps] => x e pps]
Iff-And, 82
84 x e pps => Set(x) & ALL(d):[d e x => d e ps]
Split, 83
Sufficient: For x e pps
85 Set(x) & ALL(d):[d e x => d e ps] => x e pps
Split, 83
86 Set(x)
Substitute, 77, 23
Prove: ALL(d):[d e x => d e ps]
Suppose...
87 y e x
Premise
88 y e t
Substitute, 77, 87
Prove: y e ps
Apply definition of t
89 y e t <=> y e ps & y=null
U Spec, 24
90 [y e t => y e ps & y=null] & [y e ps & y=null => y e t]
Iff-And, 89
91 y e t => y e ps & y=null
Split, 90
92 y e ps & y=null => y e t
Split, 90
93 y e ps & y=null
Detach, 91, 88
As Required:
94 y e ps
Split, 93
As Required:
95 ALL(d):[d e x => d e ps]
4 Conclusion, 87
96 Set(x) & ALL(d):[d e x => d e ps]
Join, 86, 95
As Required:
97 x e pps
Detach, 85, 96
98 x e pps & x=t
Join, 97, 77
As Required:
99 x e u
Detach, 81, 98
As Required:
100 ALL(a):[a=t => a e u]
4 Conclusion, 77
101 ALL(a):[[a e u => a=t] & [a=t => a e u]]
Join, 76, 100
As Required:
102 ALL(a):[a e u <=> a=t]
Iff-And, 101
Prove: t e u
Apply definition of u
103 t e u <=> t e pps & t=t
U Spec, 67
104 [t e u => t e pps & t=t] & [t e pps & t=t => t e u]
Iff-And, 103
105 t e u => t e pps & t=t
Split, 104
Sufficient: For t e u
106 t e pps & t=t => t e u
Split, 104
Prove: t e pps
Apply definition of pps
107 t e pps <=> Set(t) & ALL(d):[d e t => d e ps]
U Spec, 63
108 [t e pps => Set(t) & ALL(d):[d e t => d e ps]]
& [Set(t) & ALL(d):[d e t => d e ps] => t e pps]
Iff-And, 107
109 t e pps => Set(t) & ALL(d):[d e t => d e ps]
Split, 108
Sufficient: For t e pps
110 Set(t) & ALL(d):[d e t => d e ps] => t e pps
Split, 108
Prove: ALL(d):[d e t => d e ps]
Suppose...
111 x e t
Premise
Prove: x e ps
Apply definition of t
112 x e t <=> x e ps & x=null
U Spec, 24
113 [x e t => x e ps & x=null] & [x e ps & x=null => x e t]
Iff-And, 112
114 x e t => x e ps & x=null
Split, 113
115 x e ps & x=null => x e t
Split, 113
116 x e ps & x=null
Detach, 114, 111
As Required:
117 x e ps
Split, 116
As Required:
118 ALL(d):[d e t => d e ps]
4 Conclusion, 111
119 Set(t) & ALL(d):[d e t => d e ps]
Join, 23, 118
As Required:
120 t e pps
Detach, 110, 119
121 t=t
Reflex
122 t e pps & t=t
Join, 120, 121
As Required:
123 t e u
Detach, 106, 122
Prove: null e t
Apply definition of t
124 null e t <=> null e ps & null=null
U Spec, 24
125 [null e t => null e ps & null=null]
& [null e ps & null=null => null e t]
Iff-And, 124
126 null e t => null e ps & null=null
Split, 125
Sufficient: For null e t
127 null e ps & null=null => null e t
Split, 125
Prove: null e ps
Apply definition of ps
128 null e ps <=> Set(null) & ALL(d):[d e null => d e s]
U Spec, 20
129 [null e ps => Set(null) & ALL(d):[d e null => d e s]]
& [Set(null) & ALL(d):[d e null => d e s] => null e ps]
Iff-And, 128
130 null e ps => Set(null) & ALL(d):[d e null => d e s]
Split, 129
Sufficient: For null e ps
131 Set(null) & ALL(d):[d e null => d e s] => null e ps
Split, 129
Prove: ALL(d):[d e null => d e s]
Suppose...
132 x e null
Premise
Prove: x e s
Apply definition of null
133 ~x e null
U Spec, 14
134 ~~x e null => x e s
Arb Cons, 133
135 x e null => x e s
Rem DNeg, 134
As Required:
136 x e s
Detach, 135, 132
As Required:
137 ALL(d):[d e null => d e s]
4 Conclusion, 132
Join results
138 Set(null) & ALL(d):[d e null => d e s]
Join, 4, 137
As Required:
139 null e ps
Detach, 131, 138
140 null=null
Reflex
141 null e ps & null=null
Join, 139, 140
As Required:
142 null e t
Detach, 127, 141
Prove: ~null e u
Apply definition of u
143 null e u <=> null e pps & null=t
U Spec, 67
144 [null e u => null e pps & null=t]
& [null e pps & null=t => null e u]
Iff-And, 143
145 null e u => null e pps & null=t
Split, 144
146 null e pps & null=t => null e u
Split, 144
147 ~[null e pps & null=t] => ~null e u
Contra, 145
148 ~~[~null e pps | ~null=t] => ~null e u
DeMorgan, 147
Sufficient: For ~null e u
149 ~null e pps | ~null=t => ~null e u
Rem DNeg, 148
Prove: ~null=t
Apply Set Equality Axiom
150 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
151 ALL(b):[Set(null) & Set(b) => [null=b <=> ALL(c):[c e null <=> c e b]]]
U Spec, 150
152 Set(null) & Set(t) => [null=t <=> ALL(c):[c e null <=> c e t]]
U Spec, 151
153 Set(null) & Set(t)
Join, 4, 23
154 null=t <=> ALL(c):[c e null <=> c e t]
Detach, 152, 153
155 [null=t => ALL(c):[c e null <=> c e t]]
& [ALL(c):[c e null <=> c e t] => null=t]
Iff-And, 154
156 null=t => ALL(c):[c e null <=> c e t]
Split, 155
157 ALL(c):[c e null <=> c e t] => null=t
Split, 155
158 ~ALL(c):[c e null <=> c e t] => ~null=t
Contra, 156
159 ~~EXIST(c):~[c e null <=> c e t] => ~null=t
Quant, 158
160 EXIST(c):~[c e null <=> c e t] => ~null=t
Rem DNeg, 159
161 EXIST(c):~[[c e null => c e t]
& [c e t => c e null]] => ~null=t
Iff-And, 160
162 EXIST(c):~~[~[c e null => c e t] | ~[c e t => c e null]] => ~null=t
DeMorgan, 161
163 EXIST(c):[~[c e null => c e t] | ~[c e t => c e null]] => ~null=t
Rem DNeg, 162
164 EXIST(c):[~~[c e null & ~c e t] | ~[c e t => c e null]] => ~null=t
Imply-And, 163
165 EXIST(c):[c e null & ~c e t | ~[c e t => c e null]] => ~null=t
Rem DNeg, 164
166 EXIST(c):[c e null & ~c e t | ~~[c e t & ~c e null]] => ~null=t
Imply-And, 165
Sufficient: For ~null=t
167 EXIST(c):[c e null & ~c e t | c e t & ~c e null] => ~null=t
Rem DNeg, 166
168 ~null e null
U Spec, 14
169 null e t & ~null e null
Join, 142, 168
170 null e null & ~null e t | null e t & ~null e null
Arb Or, 169
Generalizing...
171 EXIST(c):[c e null & ~c e t | c e t & ~c e null]
E Gen, 170
As Required:
172 ~null=t
Detach, 167, 171
173 ~null e pps | ~null=t
Arb Or, 172
174 ~null e u
Detach, 149, 173
175 null e t & ~null e u
Join, 142, 174
Generalizing...
176 EXIST(c):[c e t & ~c e u]
E Gen, 175
177 ~ALL(c):~[c e t & ~c e u]
Quant, 176
178 ~ALL(c):~~[c e t => ~~c e u]
Imply-And, 177
179 ~ALL(c):[c e t => ~~c e u]
Rem DNeg, 178
As Required:
180 ~ALL(c):[c e t => c e u]
Rem DNeg, 179
181 Set(t) & Set(u)
Join, 23, 66
182 Set(t) & Set(u) & t e u
Join, 181, 123
183 Set(t) & Set(u) & t e u
& ~ALL(c):[c e t => c e u]
Join, 182, 180
As Required:
184 ALL(s):[Set(s)
=> EXIST(a):EXIST(b):[Set(a) & Set(b) & a e b
& ~ALL(c):[c e a => c e b]]]
4 Conclusion, 1