Theorem oa4uto4g 975

Description: Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974. (Contributed by NM, 28-Dec-1998.)

Hypotheses

Ref	Expression
oa4uto4g.1	((b⊥ →1 d) ∩ ((b⊥ ⊥ →1 d) ∪ ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))))))) ≤ d
oa4uto4g.4	h = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))

Assertion

Ref	Expression
oa4uto4g	((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)) ≤ (b →1 d)

Proof of Theorem oa4uto4g

Step	Hyp	Ref	Expression
1		ancom 74	. . . . . . . 8 (a ∩ b) = (b ∩ a)
2		ancom 74	. . . . . . . 8 ((a →1 d) ∩ (b →1 d)) = ((b →1 d) ∩ (a →1 d))
3	1, 2	2or 72	. . . . . . 7 ((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) = ((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d)))
4	3	ax-r5 38	. . . . . 6 (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h) = (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h)
5	4	lan 77	. . . . 5 ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)) = ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h))
6	5	lor 70	. . . 4 ((b →1 d) ∪ ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h))) = ((b →1 d) ∪ ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h)))
7	6	lan 77	. . 3 (b ∩ ((b →1 d) ∪ ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)))) = (b ∩ ((b →1 d) ∪ ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h))))
8		u1lem9a 777	. . . . . 6 (b⊥ →1 d)⊥ ≤ b⊥
9	8	lecon1 155	. . . . 5 b ≤ (b⊥ →1 d)
10		u1lem9a 777	. . . . . . . . . . 11 (a⊥ →1 d)⊥ ≤ a⊥
11	10	lecon1 155	. . . . . . . . . 10 a ≤ (a⊥ →1 d)
12	9, 11	le2an 169	. . . . . . . . 9 (b ∩ a) ≤ ((b⊥ →1 d) ∩ (a⊥ →1 d))
13	12	leror 152	. . . . . . . 8 ((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ≤ (((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d)))
14		oa4uto4g.4	. . . . . . . . 9 h = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))
15		u1lem9a 777	. . . . . . . . . . . . 13 (c⊥ →1 d)⊥ ≤ c⊥
16	15	lecon1 155	. . . . . . . . . . . 12 c ≤ (c⊥ →1 d)
17	11, 16	le2an 169	. . . . . . . . . . 11 (a ∩ c) ≤ ((a⊥ →1 d) ∩ (c⊥ →1 d))
18	17	leror 152	. . . . . . . . . 10 ((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ≤ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d)))
19	9, 16	le2an 169	. . . . . . . . . . 11 (b ∩ c) ≤ ((b⊥ →1 d) ∩ (c⊥ →1 d))
20	19	leror 152	. . . . . . . . . 10 ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))) ≤ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))
21	18, 20	le2an 169	. . . . . . . . 9 (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))) ≤ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))
22	14, 21	bltr 138	. . . . . . . 8 h ≤ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))
23	13, 22	le2or 168	. . . . . . 7 (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h) ≤ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))))
24	23	lelan 167	. . . . . 6 ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h)) ≤ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))))
25	24	lelor 166	. . . . 5 ((b →1 d) ∪ ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h))) ≤ ((b →1 d) ∪ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))))))
26	9, 25	le2an 169	. . . 4 (b ∩ ((b →1 d) ∪ ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h)))) ≤ ((b⊥ →1 d) ∩ ((b →1 d) ∪ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))))))
27		ax-a1 30	. . . . . . . 8 b = b⊥ ⊥
28	27	ud1lem0b 256	. . . . . . 7 (b →1 d) = (b⊥ ⊥ →1 d)
29		ax-a1 30	. . . . . . . . 9 a = a⊥ ⊥
30	29	ud1lem0b 256	. . . . . . . 8 (a →1 d) = (a⊥ ⊥ →1 d)
31	28, 30	2an 79	. . . . . . . . . 10 ((b →1 d) ∩ (a →1 d)) = ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))
32	31	lor 70	. . . . . . . . 9 (((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) = (((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d)))
33		ancom 74	. . . . . . . . . 10 ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))) = ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))))
34		ax-a1 30	. . . . . . . . . . . . . 14 c = c⊥ ⊥
35	34	ud1lem0b 256	. . . . . . . . . . . . 13 (c →1 d) = (c⊥ ⊥ →1 d)
36	28, 35	2an 79	. . . . . . . . . . . 12 ((b →1 d) ∩ (c →1 d)) = ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))
37	36	lor 70	. . . . . . . . . . 11 (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))) = (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))
38	30, 35	2an 79	. . . . . . . . . . . 12 ((a →1 d) ∩ (c →1 d)) = ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))
39	38	lor 70	. . . . . . . . . . 11 (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) = (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))
40	37, 39	2an 79	. . . . . . . . . 10 ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d)))) = ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))))
41	33, 40	ax-r2 36	. . . . . . . . 9 ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))) = ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))))
42	32, 41	2or 72	. . . . . . . 8 ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))) = ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))))
43	30, 42	2an 79	. . . . . . 7 ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))))) = ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))))))
44	28, 43	2or 72	. . . . . 6 ((b →1 d) ∪ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d))))))) = ((b⊥ ⊥ →1 d) ∪ ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))))))
45	44	lan 77	. . . . 5 ((b⊥ →1 d) ∩ ((b →1 d) ∪ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))))))) = ((b⊥ →1 d) ∩ ((b⊥ ⊥ →1 d) ∪ ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))))))))
46		oa4uto4g.1	. . . . 5 ((b⊥ →1 d) ∩ ((b⊥ ⊥ →1 d) ∪ ((a⊥ ⊥ →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (a⊥ ⊥ →1 d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1 d) ∩ (c⊥ ⊥ →1 d)))))))) ≤ d
47	45, 46	bltr 138	. . . 4 ((b⊥ →1 d) ∩ ((b →1 d) ∪ ((a →1 d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (a →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a →1 d) ∩ (c →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b →1 d) ∩ (c →1 d)))))))) ≤ d
48	26, 47	letr 137	. . 3 (b ∩ ((b →1 d) ∪ ((a →1 d) ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ h)))) ≤ d
49	7, 48	bltr 138	. 2 (b ∩ ((b →1 d) ∪ ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)))) ≤ d
50	49	oau 929	1 ((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ h)) ≤ (b →1 d)

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

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  4oa  1039