Theorem oa6fromdualn 954

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

Hypothesis

Ref	Expression
oa6fromdualn.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
oa6fromdualn	(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))

Proof of Theorem oa6fromdualn

Step	Hyp	Ref	Expression
1		oa6fromdualn.1	. . 3 (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))
2		ax-a1 30	. . . 4 b = b⊥ ⊥
3		ax-a1 30	. . . . 5 a = a⊥ ⊥
4		ax-a1 30	. . . . . 6 c = c⊥ ⊥
5	3, 4	2an 79	. . . . . . . 8 (a ∩ c) = (a⊥ ⊥ ∩ c⊥ ⊥ )
6		ax-a1 30	. . . . . . . . 9 d = d⊥ ⊥
7	2, 6	2an 79	. . . . . . . 8 (b ∩ d) = (b⊥ ⊥ ∩ d⊥ ⊥ )
8	5, 7	2or 72	. . . . . . 7 ((a ∩ c) ∪ (b ∩ d)) = ((a⊥ ⊥ ∩ c⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ d⊥ ⊥ ))
9		ax-a1 30	. . . . . . . . . 10 e = e⊥ ⊥
10	3, 9	2an 79	. . . . . . . . 9 (a ∩ e) = (a⊥ ⊥ ∩ e⊥ ⊥ )
11		ax-a1 30	. . . . . . . . . 10 f = f⊥ ⊥
12	2, 11	2an 79	. . . . . . . . 9 (b ∩ f) = (b⊥ ⊥ ∩ f⊥ ⊥ )
13	10, 12	2or 72	. . . . . . . 8 ((a ∩ e) ∪ (b ∩ f)) = ((a⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ f⊥ ⊥ ))
14	4, 9	2an 79	. . . . . . . . 9 (c ∩ e) = (c⊥ ⊥ ∩ e⊥ ⊥ )
15	6, 11	2an 79	. . . . . . . . 9 (d ∩ f) = (d⊥ ⊥ ∩ f⊥ ⊥ )
16	14, 15	2or 72	. . . . . . . 8 ((c ∩ e) ∪ (d ∩ f)) = ((c⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (d⊥ ⊥ ∩ f⊥ ⊥ ))
17	13, 16	2an 79	. . . . . . 7 (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))) = (((a⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ f⊥ ⊥ )) ∩ ((c⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (d⊥ ⊥ ∩ f⊥ ⊥ )))
18	8, 17	2or 72	. . . . . 6 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f)))) = (((a⊥ ⊥ ∩ c⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ d⊥ ⊥ )) ∪ (((a⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ f⊥ ⊥ )) ∩ ((c⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (d⊥ ⊥ ∩ f⊥ ⊥ ))))
19	4, 18	2an 79	. . . . 5 (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⊥ ⊥ )))))
20	3, 19	2or 72	. . . 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⊥ ⊥ ))))))
21	2, 20	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⊥ ⊥ )))))))
22	3, 2	2an 79	. . . . 5 (a ∩ b) = (a⊥ ⊥ ∩ b⊥ ⊥ )
23	4, 6	2an 79	. . . . 5 (c ∩ d) = (c⊥ ⊥ ∩ d⊥ ⊥ )
24	22, 23	2or 72	. . . 4 ((a ∩ b) ∪ (c ∩ d)) = ((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (c⊥ ⊥ ∩ d⊥ ⊥ ))
25	9, 11	2an 79	. . . 4 (e ∩ f) = (e⊥ ⊥ ∩ f⊥ ⊥ )
26	24, 25	2or 72	. . 3 (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f)) = (((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (c⊥ ⊥ ∩ d⊥ ⊥ )) ∪ (e⊥ ⊥ ∩ f⊥ ⊥ ))
27	1, 21, 26	le3tr2 141	. 2 (b⊥ ⊥ ∩ (a⊥ ⊥ ∪ (c⊥ ⊥ ∩ (((a⊥ ⊥ ∩ c⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ d⊥ ⊥ )) ∪ (((a⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (b⊥ ⊥ ∩ f⊥ ⊥ )) ∩ ((c⊥ ⊥ ∩ e⊥ ⊥ ) ∪ (d⊥ ⊥ ∩ f⊥ ⊥ ))))))) ≤ (((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (c⊥ ⊥ ∩ d⊥ ⊥ )) ∪ (e⊥ ⊥ ∩ f⊥ ⊥ ))
28	27	oa6fromdual 953	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: (None)