Theorem oa6fromdual 953

Description: Dual to conventional 6-variable OA law. (Contributed by NM, 22-Dec-1998.)

Hypothesis

Ref	Expression
oa6fromdual.1	(b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))

Assertion

Ref	Expression
oa6fromdual	(((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

Proof of Theorem oa6fromdual

Step	Hyp	Ref	Expression
1		oa6fromdual.1	. . 3 (b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
2	1	lecon 154	. 2 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))⊥ ≤ (b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))))⊥
3		oran 87	. . . . . 6 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
4		oran 87	. . . . . 6 (c ∪ d) = (c⊥ ∩ d⊥ )⊥
5	3, 4	2an 79	. . . . 5 ((a ∪ b) ∩ (c ∪ d)) = ((a⊥ ∩ b⊥ )⊥ ∩ (c⊥ ∩ d⊥ )⊥ )
6		anor3 90	. . . . 5 ((a⊥ ∩ b⊥ )⊥ ∩ (c⊥ ∩ d⊥ )⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))⊥
7	5, 6	ax-r2 36	. . . 4 ((a ∪ b) ∩ (c ∪ d)) = ((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))⊥
8		oran 87	. . . 4 (e ∪ f) = (e⊥ ∩ f⊥ )⊥
9	7, 8	2an 79	. . 3 (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))⊥ ∩ (e⊥ ∩ f⊥ )⊥ )
10		anor3 90	. . 3 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))⊥ ∩ (e⊥ ∩ f⊥ )⊥ ) = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))⊥
11	9, 10	ax-r2 36	. 2 (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))⊥
12		ax-a1 30	. . . 4 b = b⊥ ⊥
13		ax-a1 30	. . . . . 6 a = a⊥ ⊥
14		ax-a1 30	. . . . . . . 8 c = c⊥ ⊥
15		oran 87	. . . . . . . . . . . 12 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
16		oran 87	. . . . . . . . . . . 12 (b ∪ d) = (b⊥ ∩ d⊥ )⊥
17	15, 16	2an 79	. . . . . . . . . . 11 ((a ∪ c) ∩ (b ∪ d)) = ((a⊥ ∩ c⊥ )⊥ ∩ (b⊥ ∩ d⊥ )⊥ )
18		anor3 90	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ )⊥ ∩ (b⊥ ∩ d⊥ )⊥ ) = ((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ ))⊥
19	17, 18	ax-r2 36	. . . . . . . . . 10 ((a ∪ c) ∩ (b ∪ d)) = ((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ ))⊥
20		oran 87	. . . . . . . . . . . . . 14 (a ∪ e) = (a⊥ ∩ e⊥ )⊥
21		oran 87	. . . . . . . . . . . . . 14 (b ∪ f) = (b⊥ ∩ f⊥ )⊥
22	20, 21	2an 79	. . . . . . . . . . . . 13 ((a ∪ e) ∩ (b ∪ f)) = ((a⊥ ∩ e⊥ )⊥ ∩ (b⊥ ∩ f⊥ )⊥ )
23		anor3 90	. . . . . . . . . . . . 13 ((a⊥ ∩ e⊥ )⊥ ∩ (b⊥ ∩ f⊥ )⊥ ) = ((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ ))⊥
24	22, 23	ax-r2 36	. . . . . . . . . . . 12 ((a ∪ e) ∩ (b ∪ f)) = ((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ ))⊥
25		oran 87	. . . . . . . . . . . . . 14 (c ∪ e) = (c⊥ ∩ e⊥ )⊥
26		oran 87	. . . . . . . . . . . . . 14 (d ∪ f) = (d⊥ ∩ f⊥ )⊥
27	25, 26	2an 79	. . . . . . . . . . . . 13 ((c ∪ e) ∩ (d ∪ f)) = ((c⊥ ∩ e⊥ )⊥ ∩ (d⊥ ∩ f⊥ )⊥ )
28		anor3 90	. . . . . . . . . . . . 13 ((c⊥ ∩ e⊥ )⊥ ∩ (d⊥ ∩ f⊥ )⊥ ) = ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))⊥
29	27, 28	ax-r2 36	. . . . . . . . . . . 12 ((c ∪ e) ∩ (d ∪ f)) = ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))⊥
30	24, 29	2or 72	. . . . . . . . . . 11 (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))) = (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ ))⊥ ∪ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))⊥ )
31		oran3 93	. . . . . . . . . . 11 (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ ))⊥ ∪ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))⊥ ) = (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))⊥
32	30, 31	ax-r2 36	. . . . . . . . . 10 (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))) = (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))⊥
33	19, 32	2an 79	. . . . . . . . 9 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))) = (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ ))⊥ ∩ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))⊥ )
34		anor3 90	. . . . . . . . 9 (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ ))⊥ ∩ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))⊥ ) = (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))⊥
35	33, 34	ax-r2 36	. . . . . . . 8 (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))) = (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))⊥
36	14, 35	2or 72	. . . . . . 7 (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))) = (c⊥ ⊥ ∪ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))⊥ )
37		oran3 93	. . . . . . 7 (c⊥ ⊥ ∪ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))⊥ ) = (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))⊥
38	36, 37	ax-r2 36	. . . . . 6 (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))) = (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))⊥
39	13, 38	2an 79	. . . . 5 (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))) = (a⊥ ⊥ ∩ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))⊥ )
40		anor3 90	. . . . 5 (a⊥ ⊥ ∩ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))⊥ ) = (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))⊥
41	39, 40	ax-r2 36	. . . 4 (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))) = (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))⊥
42	12, 41	2or 72	. . 3 (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))))) = (b⊥ ⊥ ∪ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))⊥ )
43		oran3 93	. . 3 (b⊥ ⊥ ∪ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))⊥ ) = (b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))))⊥
44	42, 43	ax-r2 36	. 2 (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))))) = (b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ )))))))⊥
45	2, 11, 44	le3tr1 140	1 (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is used by:  oa6fromdualn  954  oa4to6  965