Power Set Theorem
-----------------

If p is the power set of s, then there can exist no function f mapping s onto p.
In some sense then, there must be "more" elements in p than in s.

Formally, we are required to prove: 

     ALL(a):ALL(b):[Set(a)
     & Set(b)
     & ALL(c):[c ε b <=> Set(c) & ALL(d):[d ε c => d ε a]]
     => ~EXIST(f):[ALL(x):[x ε a => f(x) ε b]
     & ALL(x):[x ε b => EXIST(x'):[x' ε a & f(x')=x]]]]

	
	Suppose p is the powerset of s.

	1	Set(s)
		& Set(p)
		& ALL(c):[c ε p <=> Set(c) & ALL(d):[d ε c => d ε s]]
		Premise

	Splitting this premise into its component parts...
	
	s is a set. This declaration will allow us to apply the set-theoretic axioms to s.

	2	Set(s)
		Split, 1

	p is a set

	3	Set(p)
		Split, 1

	p is the power set of s

	4	ALL(c):[c ε p <=> Set(c) & ALL(d):[d ε c => d ε s]]
		Split, 1

		
		Prove: ~[ALL(x):[x ε s => f(x) ε p]
		       & ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		
		Suppose to the contrary. Let f be a surjective function mapping s onto its power set p.

		5	ALL(x):[x ε s => f(x) ε p]
			& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]
			Premise

		Splitting this premise into its component parts...
		
		f is a function making elements of s to p

		6	ALL(x):[x ε s => f(x) ε p]
			Split, 5

		Every element of p is assumed to have a pre-image in s, i.e. f is surjective

		7	ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]
			Split, 5

		Apply the Subset axiom

		8	EXIST(a):[Set(a) & ALL(b):[b ε a <=> b ε s & ~b ε f(b)]]
			Subset, 2

		Define: k, the subset of those and only those elements of s that are 
		        not elements of their image under f

		9	Set(k) & ALL(b):[b ε k <=> b ε s & ~b ε f(b)]
			E Spec, 8

		Splitting...

		10	Set(k)
			Split, 9

		11	ALL(b):[b ε k <=> b ε s & ~b ε f(b)]
			Split, 9

		Apply the definition of f for x=k

		12	k ε p => EXIST(x'):[x' ε s & f(x')=k]
			U Spec, 7

		Prove: kεp
		
		Apply the definition of p for c=k

		13	k ε p <=> Set(k) & ALL(d):[d ε k => d ε s]
			U Spec, 4

		Split this biconditional statement

		14	[k ε p => Set(k) & ALL(d):[d ε k => d ε s]]
			& [Set(k) & ALL(d):[d ε k => d ε s] => k ε p]
			Iff-And, 13

		15	k ε p => Set(k) & ALL(d):[d ε k => d ε s]
			Split, 14

		Sufficient: For k ε p

		16	Set(k) & ALL(d):[d ε k => d ε s] => k ε p
			Split, 14

			
			Prove: x ε k => x ε s
			
			Suppose...

			17	x ε k
				Premise

			Apply the definition of k for b=x

			18	x ε k <=> x ε s & ~x ε f(x)
				U Spec, 11

			Split this biconditional statement

			19	[x ε k => x ε s & ~x ε f(x)]
				& [x ε s & ~x ε f(x) => x ε k]
				Iff-And, 18

			20	x ε k => x ε s & ~x ε f(x)
				Split, 19

			21	x ε s & ~x ε f(x) => x ε k
				Split, 19

			Apply detachment on lines 20 and 17

			22	x ε s & ~x ε f(x)
				Detach, 20, 17

			23	x ε s
				Split, 22

		As Required:

		24	x ε k => x ε s
			Conclusion, 17

		Generalizing...

		25	ALL(a):[a ε k => a ε s]
			U Gen, 24

		Join results

		26	Set(k) & ALL(a):[a ε k => a ε s]
			Join, 10, 25

		As Required:

		27	k ε p
			Detach, 16, 26

		From the definition of k...

		28	EXIST(x'):[x' ε s & f(x')=k]
			Detach, 12, 27

		Define: k', the pre-image of k under f.

		29	k' ε s & f(k')=k
			E Spec, 28

		Splitting...

		30	k' ε s
			Split, 29

		31	f(k')=k
			Split, 29

		Is k' ε k? 
		
		Apply the definition of k for b=k'

		32	k' ε k <=> k' ε s & ~k' ε f(k')
			U Spec, 11

		Substituting...

		33	k' ε k <=> k' ε s & ~k' ε k
			Substitute, 31, 32

		Split this biconditional statement

		34	[k' ε k => k' ε s & ~k' ε k]
			& [k' ε s & ~k' ε k => k' ε k]
			Iff-And, 33

		35	k' ε k => k' ε s & ~k' ε k
			Split, 34

		36	k' ε s & ~k' ε k => k' ε k
			Split, 34

			Prove: ~ k' ε k
			
			Suppose to the contrary...

			37	k' ε k
				Premise

			From the definition of k...

			38	k' ε s & ~k' ε k
				Detach, 35, 37

			Splitting...

			39	k' ε s
				Split, 38

			40	~k' ε k
				Split, 38

			Obtain the contradiction...

			41	k' ε k & ~k' ε k
				Join, 37, 40

		As Required:

		42	~k' ε k
			Conclusion, 37

		43	k' ε s & ~k' ε k
			Join, 30, 42

		From the definition of k...

		44	k' ε k
			Detach, 36, 43

		Obtain the contradiction...

		45	~k' ε k & k' ε k
			Join, 42, 44

	As Required:

	46	~[ALL(x):[x ε s => f(x) ε p]
		& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		Conclusion, 5

	Generalizing...

	47	ALL(f):~[ALL(x):[x ε s => f(x) ε p]
		& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		U Gen, 46

	Switch quantifier

	48	~EXIST(f):~~[ALL(x):[x ε s => f(x) ε p]
		& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		Quant, 47

	Remove the double negation

	49	~EXIST(f):[ALL(x):[x ε s => f(x) ε p]
		& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		Rem DNeg, 48

As Required:

50	Set(s)
	& Set(p)
	& ALL(c):[c ε p <=> Set(c) & ALL(d):[d ε c => d ε s]]
	=> ~EXIST(f):[ALL(x):[x ε s => f(x) ε p]
	& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
	Conclusion, 1

Generalizing...

51	ALL(b):[Set(s)
	& Set(b)
	& ALL(c):[c ε b <=> Set(c) & ALL(d):[d ε c => d ε s]]
	=> ~EXIST(f):[ALL(x):[x ε s => f(x) ε b]
	& ALL(x):[x ε b => EXIST(x'):[x' ε s & f(x')=x]]]]
	U Gen, 50

As Required:

52	ALL(a):ALL(b):[Set(a)
	& Set(b)
	& ALL(c):[c ε b <=> Set(c) & ALL(d):[d ε c => d ε a]]
	=> ~EXIST(f):[ALL(x):[x ε a => f(x) ε b]
	& ALL(x):[x ε b => EXIST(x'):[x' ε a & f(x')=x]]]]
	U Gen, 51