The Power Set Theorem

Theorem
-------

If p is the powerset of s, then there exists no function mapping s to every element of p.
Thus, the powerset of any set s, finite or otherwise, is always larger than s.

Here, the Subset Axiom is used to create an contradiction in an indirect proof.

	
	Proof
	-----
	
	Let p be the powerset of s

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

	Split premise

	2	Set(s)
		Split, 1

	3	Set(p)
		Split, 1

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

		Let f be a function mapping s to every element of p. Obtain a contradiction.

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

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

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

		Construct set k

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

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

		Define: k, the subset of s that is not a element of its image under f

		10	Set(k)
			Split, 9

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

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

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

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

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

		Sufficient: For k ε p

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

			Prove: ALL(d):[d ε k => d ε s]
			
			Suppose...

			16	x ε k
				Premise

			Apply definition of k

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

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

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

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

			21	x ε s & ~x ε f(x)
				Detach, 19, 16

			22	x ε s
				Split, 21

		As Required:

		23	ALL(d):[d ε k => d ε s]
			Conclusion, 16
		24	Set(k) & ALL(d):[d ε k => d ε s]
			Join, 10, 23

		As Required:

		25	k ε p
			Detach, 15, 24

		Apply definition of f

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

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

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

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

		29	k' ε s
			Split, 28

		30	f(k')=k
			Split, 28

		Is k' ε k? Apply the definition of k

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

		Substitute

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

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

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

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

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

			36	k' ε k
				Premise

			37	k' ε s & ~k' ε k
				Detach, 34, 36

			38	k' ε s
				Split, 37

			39	~k' ε k
				Split, 37

			40	k' ε k & ~k' ε k
				Join, 36, 39

		As Required:

		41	~k' ε k
			Conclusion, 36
		42	k' ε s & ~k' ε k
			Join, 29, 41

		43	k' ε k
			Detach, 35, 42

		We obtain the contradiction...

		44	~k' ε k & k' ε k
			Join, 41, 43

	As Required:

	45	ALL(f):~[ALL(x):[x ε s => f(x) ε p]
		& ALL(x):[x ε p => EXIST(x'):[x' ε s & f(x')=x]]]
		Conclusion, 5
	Change quantifier and remove ~~

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

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

As Required:

48	ALL(s):ALL(p):[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