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