Prove: 

ALL(x):ALL(y):ALL(z):[x  pu
& y  pu
& z  pu
& ALL(a):[a  x => a  z]
& ALL(a):[a  y => a  z]
=> ALL(a):[a  x&&y => a  z]
& ALL(a):[a  x||y => a  z]]

where 

pu is the power set of a "universal" set u
&& is the pairwise intersection operator on pu
|| is the pairwise union operator on pu

We begin by defining the set operators for a universal 
set u (lines 1 through 10).


Let u be a "universal" set. (Actually just an arbitrary set.)

1	Set(u)
	Premise

Define: Set operators &&, ||, ` (built into DC Proof)

2	ALL(a):[Set(a) => EXIST(b):[Set(b) & ALL(c):[c  b <=> Set(c) & ALL(d):[d  c => d  a]]
	& ALL(c):ALL(d):[c  b & d  b => Set(c||d) & c||d  b & ALL(e):[e  c||d <=> e  c | e  d]]
	& ALL(c):ALL(d):[c  b & d  b => Set(c&&d) & c&&d  b & ALL(e):[e  c&&d <=> e  c & e  d]]
	& ALL(c):[c  b => Set(`c) & `c  b & ALL(d):[d  `c <=> d  a & ~d  c]]]]
	Set Ops

Apply definition of set operators for set u.

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

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

Define: pu, the power set of u with operators ||, && and `

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

6	Set(pu)
	Split, 5

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

Define: Pairwise union operator (||) on pu

8	ALL(c):ALL(d):[c  pu & d  pu => Set(c||d) & c||d  pu & ALL(e):[e  c||d <=> e  c | e  d]]
	Split, 5

Define: Pairwise intersection operator (&&) on pu

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

Define: Set complement operator (`) on pu

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

	
	Prove: 
	
	x  pu
	& y  pu
	& z  pu
	& ALL(a):[a  x => a  z]
	& ALL(a):[a  y => a  z]
	=> ALL(a):[a  x&&y => a  z]
	& ALL(a):[a  x||y => a  z]
	
	Suppose...

	11	x  pu
		& y  pu
		& z  pu
		& ALL(a):[a  x => a  z]
		& ALL(a):[a  y => a  z]
		Premise

	12	x  pu
		Split, 11

	13	y  pu
		Split, 11

	14	z  pu
		Split, 11

	x is a subset of z

	15	ALL(a):[a  x => a  z]
		Split, 11

	y is a subset of z

	16	ALL(a):[a  y => a  z]
		Split, 11

		
		Prove: q  x&&y => q  z
		
		Suppose...

		17	q  x&&y
			Premise

		Applying the definition of &&...

		18	ALL(d):[x  pu & d  pu => Set(x&&d) & x&&d  pu & ALL(e):[e  x&&d <=> e  x & e  d]]
			U Spec, 9

		19	x  pu & y  pu => Set(x&&y) & x&&y  pu & ALL(e):[e  x&&y <=> e  x & e  y]
			U Spec, 18

		20	x  pu & y  pu
			Join, 12, 13

		21	Set(x&&y) & x&&y  pu & ALL(e):[e  x&&y <=> e  x & e  y]
			Detach, 19, 20

		22	Set(x&&y)
			Split, 21

		23	x&&y  pu
			Split, 21

		24	ALL(e):[e  x&&y <=> e  x & e  y]
			Split, 21

		25	q  x&&y <=> q  x & q  y
			U Spec, 24

		26	[q  x&&y => q  x & q  y]
			& [q  x & q  y => q  x&&y]
			Iff-And, 25

		27	q  x&&y => q  x & q  y
			Split, 26

		28	q  x & q  y => q  x&&y
			Split, 26

		From the definition of &&...

		29	q  x & q  y
			Detach, 27, 17

		30	q  x
			Split, 29

		31	q  y
			Split, 29

		Since x is a subset of z...

		32	q  x => q  z
			U Spec, 15

		33	q  z
			Detach, 32, 30

	As Required:

	34	q  x&&y => q  z
		Conclusion, 17

	Generalizing...

	35	ALL(a):[a  x&&y => a  z]
		U Gen, 34

		
		Prove: q  x||y => q  z
		
		Suppose...

		36	q  x||y
			Premise

		Applying the definition of ||...

		37	ALL(d):[x  pu & d  pu => Set(x||d) & x||d  pu & ALL(e):[e  x||d <=> e  x | e  d]]
			U Spec, 8

		38	x  pu & y  pu => Set(x||y) & x||y  pu & ALL(e):[e  x||y <=> e  x | e  y]
			U Spec, 37

		39	x  pu & y  pu
			Join, 12, 13

		40	Set(x||y) & x||y  pu & ALL(e):[e  x||y <=> e  x | e  y]
			Detach, 38, 39

		41	Set(x||y)
			Split, 40

		42	x||y  pu
			Split, 40

		43	ALL(e):[e  x||y <=> e  x | e  y]
			Split, 40

		44	q  x||y <=> q  x | q  y
			U Spec, 43

		45	[q  x||y => q  x | q  y]
			& [q  x | q  y => q  x||y]
			Iff-And, 44

		46	q  x||y => q  x | q  y
			Split, 45

		47	q  x | q  y => q  x||y
			Split, 45

		Two cases...

		48	q  x | q  y
			Detach, 46, 36

		Since x is a subset of z...

		49	q  x => q  z
			U Spec, 15

		50	q  y => q  z
			U Spec, 16

		51	[q  x => q  z] & [q  y => q  z]
			Join, 49, 50

		By cases...

		52	q  z
			Cases, 48, 51

	As Required:

	53	q  x||y => q  z
		Conclusion, 36

	As Required:

	54	ALL(a):[a  x||y => a  z]
		U Gen, 53

	55	ALL(a):[a  x&&y => a  z]
		& ALL(a):[a  x||y => a  z]
		Join, 35, 54

As Required:

56	x  pu
	& y  pu
	& z  pu
	& ALL(a):[a  x => a  z]
	& ALL(a):[a  y => a  z]
	=> ALL(a):[a  x&&y => a  z]
	& ALL(a):[a  x||y => a  z]
	Conclusion, 11

Generalizing...

57	ALL(z):[x  pu
	& y  pu
	& z  pu
	& ALL(a):[a  x => a  z]
	& ALL(a):[a  y => a  z]
	=> ALL(a):[a  x&&y => a  z]
	& ALL(a):[a  x||y => a  z]]
	U Gen, 56

58	ALL(y):ALL(z):[x  pu
	& y  pu
	& z  pu
	& ALL(a):[a  x => a  z]
	& ALL(a):[a  y => a  z]
	=> ALL(a):[a  x&&y => a  z]
	& ALL(a):[a  x||y => a  z]]
	U Gen, 57

As Required:

59	ALL(x):ALL(y):ALL(z):[x  pu
	& y  pu
	& z  pu
	& ALL(a):[a  x => a  z]
	& ALL(a):[a  y => a  z]
	=> ALL(a):[a  x&&y => a  z]
	& ALL(a):[a  x||y => a  z]]
	U Gen, 58