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