Theorem oa4v3v 934

Description: 4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV). (Contributed by NM, 28-Nov-1998.)

Hypotheses

Ref	Expression
oa4v3v.1	d ≤ b⊥
oa4v3v.2	e ≤ c⊥
oa4v3v.3	((d ∪ b) ∩ (e ∪ c)) ≤ (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))))
oa4v3v.4	d = (a →2 b)⊥
oa4v3v.5	e = (a →2 c)⊥

Assertion

Ref	Expression
oa4v3v	(b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))

Proof of Theorem oa4v3v

Step	Hyp	Ref	Expression
1		oa4v3v.3	. . 3 ((d ∪ b) ∩ (e ∪ c)) ≤ (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))))
2		ax-a2 31	. . . . . 6 (d ∪ b) = (b ∪ d)
3		oa4v3v.4	. . . . . . 7 d = (a →2 b)⊥
4	3	lor 70	. . . . . 6 (b ∪ d) = (b ∪ (a →2 b)⊥ )
5		oran1 91	. . . . . 6 (b ∪ (a →2 b)⊥ ) = (b⊥ ∩ (a →2 b))⊥
6	2, 4, 5	3tr 65	. . . . 5 (d ∪ b) = (b⊥ ∩ (a →2 b))⊥
7		ax-a2 31	. . . . . 6 (e ∪ c) = (c ∪ e)
8		oa4v3v.5	. . . . . . 7 e = (a →2 c)⊥
9	8	lor 70	. . . . . 6 (c ∪ e) = (c ∪ (a →2 c)⊥ )
10		oran1 91	. . . . . 6 (c ∪ (a →2 c)⊥ ) = (c⊥ ∩ (a →2 c))⊥
11	7, 9, 10	3tr 65	. . . . 5 (e ∪ c) = (c⊥ ∩ (a →2 c))⊥
12	6, 11	2an 79	. . . 4 ((d ∪ b) ∩ (e ∪ c)) = ((b⊥ ∩ (a →2 b))⊥ ∩ (c⊥ ∩ (a →2 c))⊥ )
13		anor3 90	. . . 4 ((b⊥ ∩ (a →2 b))⊥ ∩ (c⊥ ∩ (a →2 c))⊥ ) = ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))⊥
14	12, 13	ax-r2 36	. . 3 ((d ∪ b) ∩ (e ∪ c)) = ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))⊥
15		ancom 74	. . . . . . . . . 10 ((d ∪ e) ∩ (b ∪ c)) = ((b ∪ c) ∩ (d ∪ e))
16	3, 8	2or 72	. . . . . . . . . . . 12 (d ∪ e) = ((a →2 b)⊥ ∪ (a →2 c)⊥ )
17		oran3 93	. . . . . . . . . . . 12 ((a →2 b)⊥ ∪ (a →2 c)⊥ ) = ((a →2 b) ∩ (a →2 c))⊥
18	16, 17	ax-r2 36	. . . . . . . . . . 11 (d ∪ e) = ((a →2 b) ∩ (a →2 c))⊥
19	18	lan 77	. . . . . . . . . 10 ((b ∪ c) ∩ (d ∪ e)) = ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))⊥ )
20		anor1 88	. . . . . . . . . 10 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))⊥ ) = ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))⊥
21	15, 19, 20	3tr 65	. . . . . . . . 9 ((d ∪ e) ∩ (b ∪ c)) = ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))⊥
22	8, 21	2or 72	. . . . . . . 8 (e ∪ ((d ∪ e) ∩ (b ∪ c))) = ((a →2 c)⊥ ∪ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))⊥ )
23		oran3 93	. . . . . . . 8 ((a →2 c)⊥ ∪ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))⊥ ) = ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))⊥
24	22, 23	ax-r2 36	. . . . . . 7 (e ∪ ((d ∪ e) ∩ (b ∪ c))) = ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))⊥
25	3, 24	2an 79	. . . . . 6 (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))) = ((a →2 b)⊥ ∩ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))⊥ )
26		anor3 90	. . . . . 6 ((a →2 b)⊥ ∩ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))⊥ ) = ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))⊥
27	25, 26	ax-r2 36	. . . . 5 (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))) = ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))⊥
28	27	lor 70	. . . 4 (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c))))) = (b ∪ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))⊥ )
29		oran1 91	. . . 4 (b ∪ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))⊥ ) = (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))))⊥
30	28, 29	ax-r2 36	. . 3 (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c))))) = (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))))⊥
31	1, 14, 30	le3tr2 141	. 2 ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))⊥ ≤ (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c))))))⊥
32	31	lecon1 155	1 (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₂ wi2 13

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:  oa43v  1028  oa63v  1032