Theorem oa6todual 952

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

Hypothesis

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

Assertion

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

Proof of Theorem oa6todual

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