THEOREM
*******
ALL(u):[Set(u) => [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
<=> EXIST(x):x e u]]
PROOF
*****
By Dan Christensen
This proof was prepared with the aid of, and mechanically verified by the author's
DC Proof software available at http://www.dcproof.com
Let u be an arbitrary set
1 Set(u)
Premise
Suppose u is non-empty
2 EXIST(x):x e u
Premise
3 x e u
E Spec, 2
2 cases to consider: (where '|' is the OR-operator)
4 ALL(y):[y e u => P(y)] | ~ALL(y):[y e u => P(y)]
Or Not
Case 1
Prove: ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
Suppose...
5 ALL(y):[y e u => P(y)]
Premise
6 P(x) => ALL(y):[y e u => P(y)]
Arb Ante, 5
7 x e u & [P(x) => ALL(y):[y e u => P(y)]]
Join, 3, 6
8 EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
E Gen, 7
Case 1
As Required:
9 ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
4 Conclusion, 5
Case 2
Prove: ~ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]
Suppose...
10 ~ALL(y):[y e u => P(y)]
Premise
Switch quantifier
11 ~~EXIST(y):~[y e u => P(y)]
Quant, 10
12 EXIST(y):~[y e u => P(y)]
Rem DNeg, 11
13 EXIST(y):~~[y e u & ~P(y)]
Imply-And, 12
14 EXIST(y):[y e u & ~P(y)]
Rem DNeg, 13
15 y e u & ~P(y)
E Spec, 14
16 y e u
Split, 15
17 ~P(y)
Split, 15
18 ~P(y) | ALL(a):[a e u => P(a)]
Arb Or, 17
19 y e u & [~P(y) | ALL(a):[a e u => P(a)]]
Join, 16, 18
20 EXIST(x):[x e u & [~P(x) | ALL(a):[a e u => P(a)]]]
E Gen, 19
21 EXIST(x):[x e u & [~~P(x) => ALL(a):[a e u => P(a)]]]
Imply-Or, 20
22 EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]
Rem DNeg, 21
Sub-case 2
As Required:
23 ~ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]
4 Conclusion, 10
Joining previous results for Cases Rule
24 [ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]]
& [~ALL(y):[y e u => P(y)]
=> EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]]
Join, 9, 23
Apply Cases Rule
25 EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]
Cases, 4, 24
As Required:
26 EXIST(x):x e u
=> EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]
4 Conclusion, 2
Suppose u is empty
27 ~EXIST(x):x e u
Premise
Switch quantifier
28 ~~ALL(x):~x e u
Quant, 27
29 ALL(x):~x e u
Rem DNeg, 28
Prove: ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
Suppose to the contrary...
30 EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
Premise
31 x e u & [P(x) => ALL(y):[y e u => P(y)]]
E Spec, 30
32 x e u
Split, 31
33 P(x) => ALL(y):[y e u => P(y)]
Split, 31
34 ~x e u
U Spec, 29
Obtain the contradiction...
35 x e u & ~x e u
Join, 32, 34
As Required:
36 ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
4 Conclusion, 30
As Required:
37 ~EXIST(x):x e u
=> ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
4 Conclusion, 27
Apply Contrapositive Rule
38 ~~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => ~~EXIST(x):x e u
Contra, 37
39 EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => ~~EXIST(x):x e u
Rem DNeg, 38
As Required:
40 EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => EXIST(x):x e u
Rem DNeg, 39
Joint previous results for Iff-And Rule
41 [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => EXIST(x):x e u]
& [EXIST(x):x e u
=> EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]]
Join, 40, 26
Apply Iff-And Rule
42 EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
<=> EXIST(x):x e u
Iff-And, 41
As Required:
43 ALL(u):[Set(u)
=> [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]
<=> EXIST(x):x e u]]
4 Conclusion, 1