Pairwise Union

This proof justifies the pairwise union operator || as defined 
in the DC Proof. 

Prove: 

ALL(setU):[Set(setU)
=> EXIST(psetU):EXIST(union):[Set(psetU)
& ALL(c):[c  psetU <=> Set(c) & ALL(d):[d  c => d  setU]]
& ALL(a):ALL(b):[a  psetU & b  psetU 
=> union(a,b)  psetU
& ALL(d):[d  union(a,b) <=> d  a | d  b]]]]

Where:

setU       = an arbitrary "universal" set
psetU      = the power set of setU
union(a,b) = the union of sets a and b

	
	Prove: 
	
	Set(u)
	=> EXIST(psetU):EXIST(union):[Set(psetU)
	& ALL(c):[c  psetU <=> Set(c) & ALL(d):[d  c => d  u]]
	& ALL(a):ALL(b):[a  psetU & b  psetU
	=> union(a,b)  psetU
	& ALL(d):[d  union(a,b) <=> d  a | d  b]]]
	
	Suppose we have an arbitrary "universal" set u...

	1	Set(u)
		Premise

	Construct the power set of u.
	
	Applying the Power Set Axiom for 1 dimension...

	2	ALL(a):[Set(a) => EXIST(b):[Set(b)
		& ALL(c):[c  b <=> Set(c) & ALL(d):[d  c => d  a]]]]
		Power Set

	3	Set(u) => EXIST(b):[Set(b)
		& ALL(c):[c  b <=> Set(c) & ALL(d):[d  c => d  u]]]
		U Spec, 2

	4	EXIST(b):[Set(b)
		& ALL(c):[c  b <=> Set(c) & ALL(d):[d  c => d  u]]]
		Detach, 3, 1

	Define: pu, the power set of u

	5	Set(pu)
		& ALL(c):[c  pu <=> Set(c) & ALL(d):[d  c => d  u]]
		E Spec, 4

	6	Set(pu)
		Split, 5

	7	ALL(c):[c  pu <=> Set(c) & ALL(d):[d  c => d  u]]
		Split, 5

	Construct the set of ordered triples of subsets of u.
	
	Applying the Cartesian Product Axiom for 3 dimensions...

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

	9	ALL(a2):ALL(a3):[Set(pu) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  b <=> c1  pu & c2  a2 & c3  a3]]]
		U Spec, 8

	10	ALL(a3):[Set(pu) & Set(pu) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  b <=> c1  pu & c2  pu & c3  a3]]]
		U Spec, 9

	11	Set(pu) & Set(pu) & Set(pu) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  b <=> c1  pu & c2  pu & c3  pu]]
		U Spec, 10

	12	Set(pu) & Set(pu)
		Join, 6, 6

	13	Set(pu) & Set(pu) & Set(pu)
		Join, 12, 6

	14	EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  b <=> c1  pu & c2  pu & c3  pu]]
		Detach, 11, 13

	Define: pu3, the set of ordered triples of subsets of u

	15	Set''(pu3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  pu3 <=> c1  pu & c2  pu & c3  pu]
		E Spec, 14

	16	Set''(pu3)
		Split, 15

	17	ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)  pu3 <=> c1  pu & c2  pu & c3  pu]
		Split, 15

	18	EXIST(uni):[Set''(uni) & ALL(a):ALL(b):ALL(c):[(a,b,c)  uni
		<=> (a,b,c)  pu3 & ALL(d):[d  c <=> d  a | d  b]]]
		Subset, 16

	Define: uni, as subset of pu (prove to be a function)

	19	Set''(uni) & ALL(a):ALL(b):ALL(c):[(a,b,c)  uni
		<=> (a,b,c)  pu3 & ALL(d):[d  c <=> d  a | d  b]]
		E Spec, 18

	20	Set''(uni)
		Split, 19

	21	ALL(a):ALL(b):ALL(c):[(a,b,c)  uni
		<=> (a,b,c)  pu3 & ALL(d):[d  c <=> d  a | d  b]]
		Split, 19

	Prove: uni is a function of 2 variables.
	
	Applying the definition functions of 2 variables...

	22	ALL(f):ALL(a1):ALL(a2):ALL(b):[Set''(f)
		& Set(a1) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1  a1 & c2  a2 => EXIST(d):[d  b & (c1,c2,d)  f]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  a1 & c2  a2 & d1  b & d2  b & (c1,c2,d1)  f & (c1,c2,d2)  f => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1  a1 & c2  a2 & d  b => [d=f(c1,c2) <=> (c1,c2,d)  f]]]
		Function

	23	ALL(a1):ALL(a2):ALL(b):[Set''(uni)
		& Set(a1) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1  a1 & c2  a2 => EXIST(d):[d  b & (c1,c2,d)  uni]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  a1 & c2  a2 & d1  b & d2  b & (c1,c2,d1)  uni & (c1,c2,d2)  uni => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1  a1 & c2  a2 & d  b => [d=uni(c1,c2) <=> (c1,c2,d)  uni]]]
		U Spec, 22

	24	ALL(a2):ALL(b):[Set''(uni)
		& Set(pu) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1  pu & c2  a2 => EXIST(d):[d  b & (c1,c2,d)  uni]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  pu & c2  a2 & d1  b & d2  b & (c1,c2,d1)  uni & (c1,c2,d2)  uni => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1  pu & c2  a2 & d  b => [d=uni(c1,c2) <=> (c1,c2,d)  uni]]]
		U Spec, 23

	25	ALL(b):[Set''(uni)
		& Set(pu) & Set(pu) & Set(b)
		& ALL(c1):ALL(c2):[c1  pu & c2  pu => EXIST(d):[d  b & (c1,c2,d)  uni]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  pu & c2  pu & d1  b & d2  b & (c1,c2,d1)  uni & (c1,c2,d2)  uni => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1  pu & c2  pu & d  b => [d=uni(c1,c2) <=> (c1,c2,d)  uni]]]
		U Spec, 24

	Sufficient: For functionality of uni

	26	Set''(uni)
		& Set(pu) & Set(pu) & Set(pu)
		& ALL(c1):ALL(c2):[c1  pu & c2  pu => EXIST(d):[d  pu & (c1,c2,d)  uni]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  pu & c2  pu & d1  pu & d2  pu & (c1,c2,d1)  uni & (c1,c2,d2)  uni => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1  pu & c2  pu & d  pu => [d=uni(c1,c2) <=> (c1,c2,d)  uni]]
		U Spec, 25

		Prove: x  pu & y  pu => EXIST(d):[d  pu & (x,y,d)  uni]
		
		Suppose...

		27	x  pu & y  pu
			Premise

		x is a subset of u

		28	x  pu
			Split, 27

		y is a subset of u

		29	y  pu
			Split, 27

		Construct the union of x and y.
		
		Applying the Subset Axiom...

		30	EXIST(xuy):[Set(xuy) & ALL(a):[a  xuy <=> a  u & [a  x | a  y]]]
			Subset, 1

		Define: xuy, the union of x and y

		31	Set(xuy) & ALL(a):[a  xuy <=> a  u & [a  x | a  y]]
			E Spec, 30

		32	Set(xuy)
			Split, 31

		33	ALL(a):[a  xuy <=> a  u & [a  x | a  y]]
			Split, 31

		Prove: (x,y,xuy)uni
		
		Applying the definition of uni..

		34	ALL(b):ALL(c):[(x,b,c)  uni
			<=> (x,b,c)  pu3 & ALL(d):[d  c <=> d  x | d  b]]
			U Spec, 21

		35	ALL(c):[(x,y,c)  uni
			<=> (x,y,c)  pu3 & ALL(d):[d  c <=> d  x | d  y]]
			U Spec, 34

		36	(x,y,xuy)  uni
			<=> (x,y,xuy)  pu3 & ALL(d):[d  xuy <=> d  x | d  y]
			U Spec, 35

		37	[(x,y,xuy)  uni => (x,y,xuy)  pu3 & ALL(d):[d  xuy <=> d  x | d  y]]
			& [(x,y,xuy)  pu3 & ALL(d):[d  xuy <=> d  x | d  y] => (x,y,xuy)  uni]
			Iff-And, 36

		38	(x,y,xuy)  uni => (x,y,xuy)  pu3 & ALL(d):[d  xuy <=> d  x | d  y]
			Split, 37

		Sufficient: For (x,y,xuy)uni

		39	(x,y,xuy)  pu3 & ALL(d):[d  xuy <=> d  x | d  y] => (x,y,xuy)  uni
			Split, 37

		Prove: (x,y,xuy)  pu3
		
		Applying the definition of pu3...

		40	ALL(c2):ALL(c3):[(x,c2,c3)  pu3 <=> x  pu & c2  pu & c3  pu]
			U Spec, 17

		41	ALL(c3):[(x,y,c3)  pu3 <=> x  pu & y  pu & c3  pu]
			U Spec, 40

		42	(x,y,xuy)  pu3 <=> x  pu & y  pu & xuy  pu
			U Spec, 41

		43	[(x,y,xuy)  pu3 => x  pu & y  pu & xuy  pu]
			& [x  pu & y  pu & xuy  pu => (x,y,xuy)  pu3]
			Iff-And, 42

		44	(x,y,xuy)  pu3 => x  pu & y  pu & xuy  pu
			Split, 43

		Sufficient: For (x,y,xuy)pu3

		45	x  pu & y  pu & xuy  pu => (x,y,xuy)  pu3
			Split, 43

		Prove: xuy  pu
		
		Applying the definition of pu...

		46	xuy  pu <=> Set(xuy) & ALL(d):[d  xuy => d  u]
			U Spec, 7

		47	[xuy  pu => Set(xuy) & ALL(d):[d  xuy => d  u]]
			& [Set(xuy) & ALL(d):[d  xuy => d  u] => xuy  pu]
			Iff-And, 46

		48	xuy  pu => Set(xuy) & ALL(d):[d  xuy => d  u]
			Split, 47

		Sufficient: For xuy  pu

		49	Set(xuy) & ALL(d):[d  xuy => d  u] => xuy  pu
			Split, 47

			Prove: p  xuy => p  u
			
			Suppose...

			50	p  xuy
				Premise

			Applying the defintion of xuy...

			51	p  xuy <=> p  u & [p  x | p  y]
				U Spec, 33

			52	[p  xuy => p  u & [p  x | p  y]]
				& [p  u & [p  x | p  y] => p  xuy]
				Iff-And, 51

			53	p  xuy => p  u & [p  x | p  y]
				Split, 52

			54	p  u & [p  x | p  y] => p  xuy
				Split, 52

			55	p  u & [p  x | p  y]
				Detach, 53, 50

			56	p  u
				Split, 55

		As Required:

		57	p  xuy => p  u
			Conclusion, 50
		Generalizing...

		58	ALL(d):[d  xuy => d  u]
			U Gen, 57

		59	Set(xuy) & ALL(d):[d  xuy => d  u]
			Join, 32, 58

		As Required:

		60	xuy  pu
			Detach, 49, 59

		61	x  pu & y  pu & xuy  pu
			Join, 27, 60

		As Required:

		62	(x,y,xuy)  pu3
			Detach, 45, 61

			
			(=>)
			
			Prove: p  xuy => p  x | p  y

			63	p  xuy
				Premise

			Applying the defintion of xuy...

			64	p  xuy <=> p  u & [p  x | p  y]
				U Spec, 33

			65	[p  xuy => p  u & [p  x | p  y]]
				& [p  u & [p  x | p  y] => p  xuy]
				Iff-And, 64

			66	p  xuy => p  u & [p  x | p  y]
				Split, 65

			67	p  u & [p  x | p  y] => p  xuy
				Split, 65

			68	p  u & [p  x | p  y]
				Detach, 66, 63

			69	p  u
				Split, 68

			70	p  x | p  y
				Split, 68

		As Required: 
		
		(=>)

		71	p  xuy => p  x | p  y
			Conclusion, 63
			
			(<=)
			
			Prove:  p  x | p  y => p  xuy
			
			Suppose (2 cases)....

			72	p  x | p  y
				Premise

			Applying the definition of xuy...

			73	p  xuy <=> p  u & [p  x | p  y]
				U Spec, 33

			74	[p  xuy => p  u & [p  x | p  y]]
				& [p  u & [p  x | p  y] => p  xuy]
				Iff-And, 73

			75	p  xuy => p  u & [p  x | p  y]
				Split, 74

			Sufficient: For p  xuy

			76	p  u & [p  x | p  y] => p  xuy
				Split, 74

				
				Prove: p  x => p  xuy  (Case 1)
				
				Suppose...

				77	p  x
					Premise

				78	x  pu <=> Set(x) & ALL(d):[d  x => d  u]
					U Spec, 7

				79	[x  pu => Set(x) & ALL(d):[d  x => d  u]]
					& [Set(x) & ALL(d):[d  x => d  u] => x  pu]
					Iff-And, 78

				80	x  pu => Set(x) & ALL(d):[d  x => d  u]
					Split, 79

				81	Set(x) & ALL(d):[d  x => d  u] => x  pu
					Split, 79

				82	Set(x) & ALL(d):[d  x => d  u]
					Detach, 80, 28

				83	Set(x)
					Split, 82

				84	ALL(d):[d  x => d  u]
					Split, 82

				85	p  x => p  u
					U Spec, 84

				86	p  u
					Detach, 85, 77

				87	p  u & [p  x | p  y]
					Join, 86, 72

				88	p  xuy
					Detach, 76, 87

			Case 1...

			89	p  x => p  xuy
				Conclusion, 77
				
				Prove: p  y => p  xuy  (Case 2)
				
				Suppose...

				90	p  y
					Premise

				Applying the definition of pu...

				91	y  pu <=> Set(y) & ALL(d):[d  y => d  u]
					U Spec, 7

				92	[y  pu => Set(y) & ALL(d):[d  y => d  u]]
					& [Set(y) & ALL(d):[d  y => d  u] => y  pu]
					Iff-And, 91

				93	y  pu => Set(y) & ALL(d):[d  y => d  u]
					Split, 92

				94	Set(y) & ALL(d):[d  y => d  u] => y  pu
					Split, 92

				95	Set(y) & ALL(d):[d  y => d  u]
					Detach, 93, 29

				96	Set(y)
					Split, 95

				97	ALL(d):[d  y => d  u]
					Split, 95

				98	p  y => p  u
					U Spec, 97

				99	p  u
					Detach, 98, 90

				100	p  u & [p  x | p  y]
					Join, 99, 72

				101	p  xuy
					Detach, 76, 100

			Case 2...

			102	p  y => p  xuy
				Conclusion, 90
			103	[p  x => p  xuy] & [p  y => p  xuy]
				Join, 89, 102

			104	p  xuy
				Cases, 72, 103

		As Required:
		
		(<=)

		105	p  x | p  y => p  xuy
			Conclusion, 72
		106	[p  xuy => p  x | p  y]
			& [p  x | p  y => p  xuy]
			Join, 71, 105

		107	p  xuy <=> p  x | p  y
			Iff-And, 106

		108	ALL(d):[d  xuy <=> d  x | d  y]
			U Gen, 107

		109	(x,y,xuy)  pu3
			& ALL(d):[d  xuy <=> d  x | d  y]
			Join, 62, 108

		From the definition of uni...

		110	(x,y,xuy)  uni
			Detach, 39, 109

		111	xuy  pu & (x,y,xuy)  uni
			Join, 60, 110

		112	EXIST(d):[d  pu & (x,y,d)  uni]
			E Gen, 111

	As Required:

	113	x  pu & y  pu => EXIST(d):[d  pu & (x,y,d)  uni]
		Conclusion, 27
	Generalizing...

	114	ALL(c2):[x  pu & c2  pu => EXIST(d):[d  pu & (x,c2,d)  uni]]
		U Gen, 113

	Images under uni exist

	115	ALL(c1):ALL(c2):[c1  pu & c2  pu => EXIST(d):[d  pu & (c1,c2,d)  uni]]
		U Gen, 114

		
		Prove: xpu & ypu & z1pu & z2pu & (x,y,z1)  uni & (x,y,z2)  uni => z1=z2
		
		Suppose..

		116	x  pu & y  pu & z1  pu & z2  pu & (x,y,z1)  uni & (x,y,z2)  uni
			Premise

		117	x  pu
			Split, 116

		118	y  pu
			Split, 116

		119	z1  pu
			Split, 116

		120	z2  pu
			Split, 116

		121	(x,y,z1)  uni
			Split, 116

		122	(x,y,z2)  uni
			Split, 116

		Applying the definition of uni...

		123	ALL(b):ALL(c):[(x,b,c)  uni
			<=> (x,b,c)  pu3 & ALL(d):[d  c <=> d  x | d  b]]
			U Spec, 21

		124	ALL(c):[(x,y,c)  uni
			<=> (x,y,c)  pu3 & ALL(d):[d  c <=> d  x | d  y]]
			U Spec, 123

		125	(x,y,z1)  uni
			<=> (x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y]
			U Spec, 124

		126	(x,y,z2)  uni
			<=> (x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y]
			U Spec, 124

		127	[(x,y,z1)  uni => (x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y]]
			& [(x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y] => (x,y,z1)  uni]
			Iff-And, 125

		128	(x,y,z1)  uni => (x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y]
			Split, 127

		129	(x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y]
			Detach, 128, 121

		130	(x,y,z1)  pu3
			Split, 129

		From the definition of uni...

		131	ALL(d):[d  z1 <=> d  x | d  y]
			Split, 129

		132	(x,y,z1)  pu3 & ALL(d):[d  z1 <=> d  x | d  y] => (x,y,z1)  uni
			Split, 127

		Applying the defintion of uni...

		133	[(x,y,z2)  uni => (x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y]]
			& [(x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y] => (x,y,z2)  uni]
			Iff-And, 126

		134	(x,y,z2)  uni => (x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y]
			Split, 133

		135	(x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y] => (x,y,z2)  uni
			Split, 133

		136	(x,y,z2)  pu3 & ALL(d):[d  z2 <=> d  x | d  y]
			Detach, 134, 122

		From the definition of uni...

		137	(x,y,z2)  pu3
			Split, 136

		138	ALL(d):[d  z2 <=> d  x | d  y]
			Split, 136

		Applying the definition of set equality...

		139	ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c  a <=> c  b]]]
			Set Equality

		140	ALL(b):[Set(z1) & Set(b) => [z1=b <=> ALL(c):[c  z1 <=> c  b]]]
			U Spec, 139

		141	Set(z1) & Set(z2) => [z1=z2 <=> ALL(c):[c  z1 <=> c  z2]]
			U Spec, 140

		Applying the definition of pu...

		142	z1  pu <=> Set(z1) & ALL(d):[d  z1 => d  u]
			U Spec, 7

		143	[z1  pu => Set(z1) & ALL(d):[d  z1 => d  u]]
			& [Set(z1) & ALL(d):[d  z1 => d  u] => z1  pu]
			Iff-And, 142

		144	z1  pu => Set(z1) & ALL(d):[d  z1 => d  u]
			Split, 143

		145	Set(z1) & ALL(d):[d  z1 => d  u] => z1  pu
			Split, 143

		146	Set(z1) & ALL(d):[d  z1 => d  u]
			Detach, 144, 119

		From the definition of pu...

		147	Set(z1)
			Split, 146

		148	ALL(d):[d  z1 => d  u]
			Split, 146

		Applying the definition of pu...

		149	z2  pu <=> Set(z2) & ALL(d):[d  z2 => d  u]
			U Spec, 7

		150	[z2  pu => Set(z2) & ALL(d):[d  z2 => d  u]]
			& [Set(z2) & ALL(d):[d  z2 => d  u] => z2  pu]
			Iff-And, 149

		151	z2  pu => Set(z2) & ALL(d):[d  z2 => d  u]
			Split, 150

		152	Set(z2) & ALL(d):[d  z2 => d  u] => z2  pu
			Split, 150

		153	Set(z2) & ALL(d):[d  z2 => d  u]
			Detach, 151, 120

		From the definition of pu...

		154	Set(z2)
			Split, 153

		155	ALL(d):[d  z2 => d  u]
			Split, 153

		156	Set(z1) & Set(z2)
			Join, 147, 154

		157	z1=z2 <=> ALL(c):[c  z1 <=> c  z2]
			Detach, 141, 156

		158	[z1=z2 => ALL(c):[c  z1 <=> c  z2]]
			& [ALL(c):[c  z1 <=> c  z2] => z1=z2]
			Iff-And, 157

		159	z1=z2 => ALL(c):[c  z1 <=> c  z2]
			Split, 158

		Sufficient: For z1=z2

		160	ALL(c):[c  z1 <=> c  z2] => z1=z2
			Split, 158

			
			Prove: p  z1 => p  z2 (=>)
			
			Suppose...

			161	p  z1
				Premise

			162	p  z2 <=> p  x | p  y
				U Spec, 138

			163	[p  z2 => p  x | p  y] & [p  x | p  y => p  z2]
				Iff-And, 162

			164	p  z2 => p  x | p  y
				Split, 163

			Sufficient: For pz2

			165	p  x | p  y => p  z2
				Split, 163

			166	p  z1 <=> p  x | p  y
				U Spec, 131

			167	[p  z1 => p  x | p  y] & [p  x | p  y => p  z1]
				Iff-And, 166

			168	p  z1 => p  x | p  y
				Split, 167

			169	p  x | p  y => p  z1
				Split, 167

			170	p  x | p  y
				Detach, 168, 161

			171	p  z2
				Detach, 165, 170

		As Required:
		
		(=>)

		172	p  z1 => p  z2
			Conclusion, 161
			Prove: p  z2 => p  z1  (<=)
			
			Suppose...

			173	p  z2
				Premise

			174	p  z1 <=> p  x | p  y
				U Spec, 131

			175	[p  z1 => p  x | p  y] & [p  x | p  y => p  z1]
				Iff-And, 174

			176	p  z1 => p  x | p  y
				Split, 175

			Sufficient: For pz1

			177	p  x | p  y => p  z1
				Split, 175

			178	p  z2 <=> p  x | p  y
				U Spec, 138

			179	[p  z2 => p  x | p  y] & [p  x | p  y => p  z2]
				Iff-And, 178

			180	p  z2 => p  x | p  y
				Split, 179

			181	p  x | p  y => p  z2
				Split, 179

			182	p  x | p  y
				Detach, 180, 173

			183	p  z1
				Detach, 177, 182

		As Required: 
		
		(<=)

		184	p  z2 => p  z1
			Conclusion, 173
		185	[p  z1 => p  z2] & [p  z2 => p  z1]
			Join, 172, 184

		186	p  z1 <=> p  z2
			Iff-And, 185

		187	ALL(c):[c  z1 <=> c  z2]
			U Gen, 186

		188	z1=z2
			Detach, 160, 187

	As Required:

	189	x  pu & y  pu & z1  pu & z2  pu & (x,y,z1)  uni & (x,y,z2)  uni
		=> z1=z2
		Conclusion, 116
	Generalizing...

	190	ALL(d2):[x  pu & y  pu & z1  pu & d2  pu & (x,y,z1)  uni & (x,y,d2)  uni
		=> z1=d2]
		U Gen, 189

	191	ALL(d1):ALL(d2):[x  pu & y  pu & d1  pu & d2  pu & (x,y,d1)  uni & (x,y,d2)  uni
		=> d1=d2]
		U Gen, 190

	192	ALL(c2):ALL(d1):ALL(d2):[x  pu & c2  pu & d1  pu & d2  pu & (x,c2,d1)  uni & (x,c2,d2)  uni
		=> d1=d2]
		U Gen, 191

	Images under uni are unique.

	193	ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  pu & c2  pu & d1  pu & d2  pu & (c1,c2,d1)  uni & (c1,c2,d2)  uni
		=> d1=d2]
		U Gen, 192

	Joining results...

	194	Set''(uni) & Set(pu)
		Join, 20, 6

	195	Set''(uni) & Set(pu) & Set(pu)
		Join, 194, 6

	196	Set''(uni) & Set(pu) & Set(pu) & Set(pu)
		Join, 195, 6

	197	Set''(uni) & Set(pu) & Set(pu) & Set(pu)
		& ALL(c1):ALL(c2):[c1  pu & c2  pu => EXIST(d):[d  pu & (c1,c2,d)  uni]]
		Join, 196, 115

	198	Set''(uni) & Set(pu) & Set(pu) & Set(pu)
		& ALL(c1):ALL(c2):[c1  pu & c2  pu => EXIST(d):[d  pu & (c1,c2,d)  uni]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1  pu & c2  pu & d1  pu & d2  pu & (c1,c2,d1)  uni & (c1,c2,d2)  uni
		=> d1=d2]
		Join, 197, 193

	uni is a function of 2 variables.

	199	ALL(c1):ALL(c2):ALL(d):[c1  pu & c2  pu & d  pu => [d=uni(c1,c2) <=> (c1,c2,d)  uni]]
		Detach, 26, 198

		
		Prove: xpu & ypu => uni(x,y)pu & ALL(d):[d  uni(x,y) <=> dx | dy]
		
		Suppose...

		200	x  pu & y  pu
			Premise

		201	x  pu
			Split, 200

		202	y  pu
			Split, 200

		203	ALL(c2):[x  pu & c2  pu => EXIST(d):[d  pu & (x,c2,d)  uni]]
			U Spec, 115

		204	x  pu & y  pu => EXIST(d):[d  pu & (x,y,d)  uni]
			U Spec, 203

		205	EXIST(d):[d  pu & (x,y,d)  uni]
			Detach, 204, 200

		206	z  pu & (x,y,z)  uni
			E Spec, 205

		207	z  pu
			Split, 206

		208	(x,y,z)  uni
			Split, 206

		209	ALL(c2):ALL(d):[x  pu & c2  pu & d  pu => [d=uni(x,c2) <=> (x,c2,d)  uni]]
			U Spec, 199

		210	ALL(d):[x  pu & y  pu & d  pu => [d=uni(x,y) <=> (x,y,d)  uni]]
			U Spec, 209

		211	x  pu & y  pu & z  pu => [z=uni(x,y) <=> (x,y,z)  uni]
			U Spec, 210

		212	x  pu & y  pu & z  pu
			Join, 200, 207

		213	z=uni(x,y) <=> (x,y,z)  uni
			Detach, 211, 212

		214	[z=uni(x,y) => (x,y,z)  uni]
			& [(x,y,z)  uni => z=uni(x,y)]
			Iff-And, 213

		215	z=uni(x,y) => (x,y,z)  uni
			Split, 214

		216	(x,y,z)  uni => z=uni(x,y)
			Split, 214

		217	z=uni(x,y)
			Detach, 216, 208

		218	uni(x,y)  pu
			Substitute, 217, 207

		219	ALL(b):ALL(c):[(x,b,c)  uni
			<=> (x,b,c)  pu3 & ALL(d):[d  c <=> d  x | d  b]]
			U Spec, 21

		220	ALL(c):[(x,y,c)  uni
			<=> (x,y,c)  pu3 & ALL(d):[d  c <=> d  x | d  y]]
			U Spec, 219

		221	(x,y,z)  uni
			<=> (x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y]
			U Spec, 220

		222	[(x,y,z)  uni => (x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y]]
			& [(x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y] => (x,y,z)  uni]
			Iff-And, 221

		223	(x,y,z)  uni => (x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y]
			Split, 222

		224	(x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y] => (x,y,z)  uni
			Split, 222

		225	(x,y,z)  pu3 & ALL(d):[d  z <=> d  x | d  y]
			Detach, 223, 208

		226	(x,y,z)  pu3
			Split, 225

		227	ALL(d):[d  z <=> d  x | d  y]
			Split, 225

		228	ALL(d):[d  uni(x,y) <=> d  x | d  y]
			Substitute, 217, 227

		229	uni(x,y)  pu
			& ALL(d):[d  uni(x,y) <=> d  x | d  y]
			Join, 218, 228

	As Required:

	230	x  pu & y  pu
		=> uni(x,y)  pu
		& ALL(d):[d  uni(x,y) <=> d  x | d  y]
		Conclusion, 200
	Generalizing...

	231	ALL(b):[x  pu & b  pu
		=> uni(x,b)  pu
		& ALL(d):[d  uni(x,b) <=> d  x | d  b]]
		U Gen, 230

	232	ALL(a):ALL(b):[a  pu & b  pu
		=> uni(a,b)  pu
		& ALL(d):[d  uni(a,b) <=> d  a | d  b]]
		U Gen, 231

	233	Set(pu)
		& ALL(c):[c  pu <=> Set(c) & ALL(d):[d  c => d  u]]
		& ALL(a):ALL(b):[a  pu & b  pu
		=> uni(a,b)  pu
		& ALL(d):[d  uni(a,b) <=> d  a | d  b]]
		Join, 5, 232

	234	EXIST(union):[Set(pu)
		& ALL(c):[c  pu <=> Set(c) & ALL(d):[d  c => d  u]]
		& ALL(a):ALL(b):[a  pu & b  pu
		=> union(a,b)  pu
		& ALL(d):[d  union(a,b) <=> d  a | d  b]]]
		E Gen, 233

	235	EXIST(psetU):EXIST(union):[Set(psetU)
		& ALL(c):[c  psetU <=> Set(c) & ALL(d):[d  c => d  u]]
		& ALL(a):ALL(b):[a  psetU & b  psetU
		=> union(a,b)  psetU
		& ALL(d):[d  union(a,b) <=> d  a | d  b]]]
		E Gen, 234


As Required:

For arbitary u...

236	Set(u)
	=> EXIST(psetU):EXIST(union):[Set(psetU)
	& ALL(c):[c  psetU <=> Set(c) & ALL(d):[d  c => d  u]]
	& ALL(a):ALL(b):[a  psetU & b  psetU
	=> union(a,b)  psetU
	& ALL(d):[d  union(a,b) <=> d  a | d  b]]]
	Conclusion, 1

As Required:

237	ALL(setU):[Set(setU)
	=> EXIST(psetU):EXIST(union):[Set(psetU)
	& ALL(c):[c  psetU <=> Set(c) & ALL(d):[d  c => d  setU]]
	& ALL(a):ALL(b):[a  psetU & b  psetU
	=> union(a,b)  psetU
	& ALL(d):[d  union(a,b) <=> d  a | d  b]]]]
	U Gen, 236