THEOREM
*******
No power set of a set is a subset of the set.
ALL(a):ALL(pa):[Set(a) & Set(pa) & ALL(x):[x e pa <=> ALL(y):[y e x => y e a]] => ~ALL(x):[x e pa => x e a]]
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
PROOF
*****
Let sets a and pa be such that pa is the power set of a
1 Set(a) & Set(pa) & ALL(x):[x e pa <=> ALL(y):[y e x => y e a]]
Premise
Splitting this premise...
2 Set(a)
Split, 1
3 Set(pa)
Split, 1
pa is the power set of a
4 ALL(x):[x e pa <=> ALL(y):[y e x => y e a]]
Split, 1
Prove: ~ALL(x):[x e pa => x e a] (i.e. pa is NOT a susbset of a)
Suppose to the contrary...
5 ALL(x):[x e pa => x e a]
Premise
Apply Subset Axiom
6 EXIST(s):[Set(s) & ALL(x):[x e s <=> x e a & ~x e x]]
Subset, 2
Let b be the subset of a such that...
7 Set(b) & ALL(x):[x e b <=> x e a & ~x e x]
E Spec, 6
Splitting...
8 Set(b)
Split, 7
9 ALL(x):[x e b <=> x e a & ~x e x]
Split, 7
Prove: b e a
Apply definition of pa
10 b e pa <=> ALL(y):[y e b => y e a]
U Spec, 4
11 [b e pa => ALL(y):[y e b => y e a]]
& [ALL(y):[y e b => y e a] => b e pa]
Iff-And, 10
12 b e pa => ALL(y):[y e b => y e a]
Split, 11
13 ALL(y):[y e b => y e a] => b e pa
Split, 11
Prove: ALL(x):[x e b => x e a]
Suppose...
14 t e b
Premise
Apply definition of b
15 t e b <=> t e a & ~t e t
U Spec, 9
16 [t e b => t e a & ~t e t] & [t e a & ~t e t => t e b]
Iff-And, 15
17 t e b => t e a & ~t e t
Split, 16
18 t e a & ~t e t => t e b
Split, 16
19 t e a & ~t e t
Detach, 17, 14
20 t e a
Split, 19
As Required:
21 ALL(x):[x e b => x e a]
4 Conclusion, 14
22 b e pa
Detach, 13, 21
Apply initial premise
23 b e pa => b e a
U Spec, 5
As Required:
24 b e a
Detach, 23, 22
Prove: b e b <=> ~b e b (contradiction)
25 b e b <=> b e a & ~b e b
U Spec, 9
26 [b e b => b e a & ~b e b] & [b e a & ~b e b => b e b]
Iff-And, 25
27 b e b => b e a & ~b e b
Split, 26
28 b e a & ~b e b => b e b
Split, 26
29 b e b
Premise
30 b e a & ~b e b
Detach, 27, 29
31 b e a
Split, 30
32 ~b e b
Split, 30
33 b e b => ~b e b
4 Conclusion, 29
34 ~b e b
Premise
35 b e a & ~b e b
Join, 24, 34
36 b e b
Detach, 28, 35
37 ~b e b => b e b
4 Conclusion, 34
38 [b e b => ~b e b] & [~b e b => b e b]
Join, 33, 37
As Required:
39 b e b <=> ~b e b
Iff-And, 38
As Required:
40 ~ALL(x):[x e pa => x e a]
4 Conclusion, 5
As Required:
41 ALL(a):ALL(pa):[Set(a) & Set(pa) & ALL(x):[x e pa <=> ALL(y):[y e x => y e a]]
=> ~ALL(x):[x e pa => x e a]]
4 Conclusion, 1