Identity Functions

Theorem
-------

Prove: ALL(s):[Set(s) => EXIST(i):ALL(a):[a ε s => a=i(a)]]

That is, on any set, empty or otherwise, there exists an identity function.

This proof makes use of the Cartesian Product and Subset Axioms of set theory to construct
a set ordered pairs that can be shown to be an identity function.

	
	Proof
	-----
	
	Suppose...

	1	Set(s)
		Premise

	Construct the Cartesian Product of s with itself.
	
	Apply the Cartesian Product axiom for 2 sets

	2	ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε a1 & c2 ε a2]]]
		Cart Prod

	3	ALL(a2):[Set(s) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε s & c2 ε a2]]]
		U Spec, 2

	4	Set(s) & Set(s) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε s & c2 ε s]]
		U Spec, 3

	5	Set(s) & Set(s)
		Join, 1, 1

	6	EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε s & c2 ε s]]
		Detach, 4, 5

	7	Set'(s2) & ALL(c1):ALL(c2):[(c1,c2) ε s2 <=> c1 ε s & c2 ε s]
		E Spec, 6

	Define: s2, the Cartesian Product of s with itself

	8	Set'(s2)
		Split, 7

	9	ALL(c1):ALL(c2):[(c1,c2) ε s2 <=> c1 ε s & c2 ε s]
		Split, 7

	Construct a subset of s2.
	
	Apply the Subset Axiom

	10	EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) ε sub <=> (a,b) ε s2 & a=b]]
		Subset, 8

	11	Set'(id) & ALL(a):ALL(b):[(a,b) ε id <=> (a,b) ε s2 & a=b]
		E Spec, 10

	Define: id, the subset of s2 with identical components
	
	Prove that id is function of 1 variable.

	12	Set'(id)
		Split, 11

	13	ALL(a):ALL(b):[(a,b) ε id <=> (a,b) ε s2 & a=b]
		Split, 11

	Apply the function axiom for 1 variable

	14	ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε f => c ε a & d ε b]
		& ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε f]]
		& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε f & (c,d2) ε f => d1=d2]
		=> ALL(c):ALL(d):[d=f(c) <=> (c,d) ε f]]
		Function

	15	ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) ε id => c ε a & d ε b]
		& ALL(c):[c ε a => EXIST(d):[d ε b & (c,d) ε id]]
		& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		=> ALL(c):ALL(d):[d=id(c) <=> (c,d) ε id]]
		U Spec, 14

	16	ALL(b):[ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε b]
		& ALL(c):[c ε s => EXIST(d):[d ε b & (c,d) ε id]]
		& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		=> ALL(c):ALL(d):[d=id(c) <=> (c,d) ε id]]
		U Spec, 15

	Sufficient: For functionality of id

	17	ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε s]
		& ALL(c):[c ε s => EXIST(d):[d ε s & (c,d) ε id]]
		& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		=> ALL(c):ALL(d):[d=id(c) <=> (c,d) ε id]
		U Spec, 16

		Part 1
		------
		
		Prove: ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε s]
		
		Suppose...

		18	(x,y) ε id
			Premise

		Apply the definition of id

		19	ALL(b):[(x,b) ε id <=> (x,b) ε s2 & x=b]
			U Spec, 13

		20	(x,y) ε id <=> (x,y) ε s2 & x=y
			U Spec, 19

		21	[(x,y) ε id => (x,y) ε s2 & x=y]
			& [(x,y) ε s2 & x=y => (x,y) ε id]
			Iff-And, 20

		22	(x,y) ε id => (x,y) ε s2 & x=y
			Split, 21

		23	(x,y) ε s2 & x=y => (x,y) ε id
			Split, 21

		24	(x,y) ε s2 & x=y
			Detach, 22, 18

		25	(x,y) ε s2
			Split, 24

		26	x=y
			Split, 24

		Apply the definition of s2

		27	ALL(c2):[(x,c2) ε s2 <=> x ε s & c2 ε s]
			U Spec, 9

		28	(x,y) ε s2 <=> x ε s & y ε s
			U Spec, 27

		29	[(x,y) ε s2 => x ε s & y ε s]
			& [x ε s & y ε s => (x,y) ε s2]
			Iff-And, 28

		30	(x,y) ε s2 => x ε s & y ε s
			Split, 29

		31	x ε s & y ε s => (x,y) ε s2
			Split, 29

		32	x ε s & y ε s
			Detach, 30, 25

	As Required: (Part 1)

	33	ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε s]
		Conclusion, 18
		Part 2
		------
		
		Prove: ALL(c):[c ε s => EXIST(d):[d ε s & (c,d) ε id]]
		
		Suppose...

		34	x ε s
			Premise

		Apply the defintion of id for a=x and b=x

		35	ALL(b):[(x,b) ε id <=> (x,b) ε s2 & x=b]
			U Spec, 13

		36	(x,x) ε id <=> (x,x) ε s2 & x=x
			U Spec, 35

		37	[(x,x) ε id => (x,x) ε s2 & x=x]
			& [(x,x) ε s2 & x=x => (x,x) ε id]
			Iff-And, 36

		38	(x,x) ε id => (x,x) ε s2 & x=x
			Split, 37

		Sufficient: For (x,x) ε id

		39	(x,x) ε s2 & x=x => (x,x) ε id
			Split, 37

		Prove: (x,x) ε s2 
		
		Apply definition of s2 for a=x and b=x

		40	ALL(c2):[(x,c2) ε s2 <=> x ε s & c2 ε s]
			U Spec, 9

		41	(x,x) ε s2 <=> x ε s & x ε s
			U Spec, 40

		42	[(x,x) ε s2 => x ε s & x ε s]
			& [x ε s & x ε s => (x,x) ε s2]
			Iff-And, 41

		43	(x,x) ε s2 => x ε s & x ε s
			Split, 42

		44	x ε s & x ε s => (x,x) ε s2
			Split, 42

		45	x ε s & x ε s
			Join, 34, 34

		46	(x,x) ε s2
			Detach, 44, 45

		47	x=x
			Reflex

		48	(x,x) ε s2 & x=x
			Join, 46, 47

		49	(x,x) ε id
			Detach, 39, 48

		50	x ε s & (x,x) ε id
			Join, 34, 49

		Generalize

		51	EXIST(d):[d ε s & (x,d) ε id]
			E Gen, 50

	As Required: (Part 2)

	52	ALL(c):[c ε s => EXIST(d):[d ε s & (c,d) ε id]]
		Conclusion, 34
		Part 3
		------
		
		Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		
		Suppose...

		53	(x,y1) ε id & (x,y2) ε id
			Premise

		54	(x,y1) ε id
			Split, 53

		55	(x,y2) ε id
			Split, 53

		Apply the definition of id for a=x and b=y1

		56	ALL(b):[(x,b) ε id <=> (x,b) ε s2 & x=b]
			U Spec, 13

		57	(x,y1) ε id <=> (x,y1) ε s2 & x=y1
			U Spec, 56

		58	[(x,y1) ε id => (x,y1) ε s2 & x=y1]
			& [(x,y1) ε s2 & x=y1 => (x,y1) ε id]
			Iff-And, 57

		59	(x,y1) ε id => (x,y1) ε s2 & x=y1
			Split, 58

		60	(x,y1) ε s2 & x=y1 => (x,y1) ε id
			Split, 58

		61	(x,y1) ε s2 & x=y1
			Detach, 59, 54

		62	(x,y1) ε s2
			Split, 61

		63	x=y1
			Split, 61

		Apply the definition of id for a=x and b=y2

		64	(x,y2) ε id <=> (x,y2) ε s2 & x=y2
			U Spec, 56

		65	[(x,y2) ε id => (x,y2) ε s2 & x=y2]
			& [(x,y2) ε s2 & x=y2 => (x,y2) ε id]
			Iff-And, 64

		66	(x,y2) ε id => (x,y2) ε s2 & x=y2
			Split, 65

		67	(x,y2) ε s2 & x=y2 => (x,y2) ε id
			Split, 65

		68	(x,y2) ε s2 & x=y2
			Detach, 66, 55

		69	(x,y2) ε s2
			Split, 68

		70	x=y2
			Split, 68

		Subsitute

		71	y1=y2
			Substitute, 63, 70

	As Required: (Part 3)

	72	ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		Conclusion, 53
	Join results

	73	ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε s]
		& ALL(c):[c ε s => EXIST(d):[d ε s & (c,d) ε id]]
		Join, 33, 52

	74	ALL(c):ALL(d):[(c,d) ε id => c ε s & d ε s]
		& ALL(c):[c ε s => EXIST(d):[d ε s & (c,d) ε id]]
		& ALL(c):ALL(d1):ALL(d2):[(c,d1) ε id & (c,d2) ε id => d1=d2]
		Join, 73, 72

	As Required: 
	
	From functionality axiom...

	75	ALL(c):ALL(d):[d=id(c) <=> (c,d) ε id]
		Detach, 17, 74

		Prove: ALL(a):[a ε s => a=id(a)]
		
		Suppose...

		76	x ε s
			Premise

		Apply above result

		77	ALL(d):[d=id(x) <=> (x,d) ε id]
			U Spec, 75

		78	x=id(x) <=> (x,x) ε id
			U Spec, 77

		79	[x=id(x) => (x,x) ε id] & [(x,x) ε id => x=id(x)]
			Iff-And, 78

		80	x=id(x) => (x,x) ε id
			Split, 79

		Sufficient: For x=id(x)

		81	(x,x) ε id => x=id(x)
			Split, 79

		Prove: (x,x)εid 
		
		Apply definition of id for a=x and b=x

		82	ALL(b):[(x,b) ε id <=> (x,b) ε s2 & x=b]
			U Spec, 13

		83	(x,x) ε id <=> (x,x) ε s2 & x=x
			U Spec, 82

		84	[(x,x) ε id => (x,x) ε s2 & x=x]
			& [(x,x) ε s2 & x=x => (x,x) ε id]
			Iff-And, 83

		85	(x,x) ε id => (x,x) ε s2 & x=x
			Split, 84

		Sufficient: For (x,x) ε id

		86	(x,x) ε s2 & x=x => (x,x) ε id
			Split, 84

		Prove: (x,x) ε s2 
		
		Apply definition of s2 for a=x and b=x

		87	ALL(c2):[(x,c2) ε s2 <=> x ε s & c2 ε s]
			U Spec, 9

		88	(x,x) ε s2 <=> x ε s & x ε s
			U Spec, 87

		89	[(x,x) ε s2 => x ε s & x ε s]
			& [x ε s & x ε s => (x,x) ε s2]
			Iff-And, 88

		90	(x,x) ε s2 => x ε s & x ε s
			Split, 89

		91	x ε s & x ε s => (x,x) ε s2
			Split, 89

		92	x ε s & x ε s
			Join, 76, 76

		93	(x,x) ε s2
			Detach, 91, 92

		94	x=x
			Reflex

		95	(x,x) ε s2 & x=x
			Join, 93, 94

		96	(x,x) ε id
			Detach, 86, 95

		97	x=id(x)
			Detach, 81, 96

	As Required:

	98	ALL(a):[a ε s => a=id(a)]
		Conclusion, 76

As Required:

99	ALL(s):[Set(s) => EXIST(i):ALL(a):[a ε s => a=i(a)]]
	Conclusion, 1