Theorem dp35lem0 1179

Description: Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)

Hypotheses

Ref	Expression
dp35lem.1	c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
dp35lem.2	c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
dp35lem.3	c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
dp35lem.4	p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
dp35lem.5	p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))

Assertion

Ref	Expression
dp35lem0	((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))

Proof of Theorem dp35lem0

Step	Hyp	Ref	Expression
1		orcom 73	. . . . . 6 ((b0 ∩ (a0 ∪ p0)) ∪ b1) = (b1 ∪ (b0 ∩ (a0 ∪ p0)))
2		leid 148	. . . . . 6 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ (b0 ∩ (a0 ∪ p0)))
3	1, 2	bltr 138	. . . . 5 ((b0 ∩ (a0 ∪ p0)) ∪ b1) ≤ (b1 ∪ (b0 ∩ (a0 ∪ p0)))
4		dp35lem.1	. . . . . 6 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
5		dp35lem.2	. . . . . 6 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
6		dp35lem.3	. . . . . 6 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
7		dp35lem.4	. . . . . 6 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
8		dp35lem.5	. . . . . 6 p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
9	4, 5, 6, 7, 8	dp35lema 1178	. . . . 5 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
10	3, 9	letr 137	. . . 4 ((b0 ∩ (a0 ∪ p0)) ∪ b1) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
11	10	lelan 167	. . 3 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
12		id 59	. . . . 5 ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
13		lea 160	. . . . . 6 ((a0 ∪ a1) ∩ (c0 ∪ c1)) ≤ (a0 ∪ a1)
14	13	mldual2i 1127	. . . . 5 ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (((a0 ∪ a1) ∩ b1) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
15	12, 14	tr 62	. . . 4 ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (((a0 ∪ a1) ∩ b1) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
16		ancom 74	. . . . 5 ((a0 ∪ a1) ∩ b1) = (b1 ∩ (a0 ∪ a1))
17	16	ror 71	. . . 4 (((a0 ∪ a1) ∩ b1) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) = ((b1 ∩ (a0 ∪ a1)) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
18	15, 17	tr 62	. . 3 ((a0 ∪ a1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = ((b1 ∩ (a0 ∪ a1)) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
19	11, 18	lbtr 139	. 2 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((b1 ∩ (a0 ∪ a1)) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
20		lear 161	. . . 4 ((a0 ∪ a1) ∩ (c0 ∪ c1)) ≤ (c0 ∪ c1)
21	20	lelor 166	. . 3 ((b1 ∩ (a0 ∪ a1)) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ ((b1 ∩ (a0 ∪ a1)) ∪ (c0 ∪ c1))
22		orcom 73	. . 3 ((b1 ∩ (a0 ∪ a1)) ∪ (c0 ∪ c1)) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
23	21, 22	lbtr 139	. 2 ((b1 ∩ (a0 ∪ a1)) ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
24	19, 23	letr 137	1 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))

Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7

This theorem was proved from 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-ml 1122  ax-arg 1153

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  dp35  1180  oadp35  1212