Theorem dp53lema 1163

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

Hypotheses

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

Assertion

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

Proof of Theorem dp53lema

Step	Hyp	Ref	Expression
1		leo 158	. 2 b1 ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
2		leo 158	. . . . . 6 (b0 ∩ (a0 ∪ p0)) ≤ ((b0 ∩ (a0 ∪ p0)) ∪ b1)
3		dp53lem.4	. . . . . . . . 9 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
4	3	lor 70	. . . . . . . 8 (a0 ∪ p0) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
5	4	lan 77	. . . . . . 7 (b0 ∩ (a0 ∪ p0)) = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
6		lear 161	. . . . . . . 8 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
7		lea 160	. . . . . . . . . 10 ((a1 ∪ b1) ∩ (a2 ∪ b2)) ≤ (a1 ∪ b1)
8	7	lelor 166	. . . . . . . . 9 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (a0 ∪ (a1 ∪ b1))
9		ax-a3 32	. . . . . . . . . 10 ((a0 ∪ a1) ∪ b1) = (a0 ∪ (a1 ∪ b1))
10	9	cm 61	. . . . . . . . 9 (a0 ∪ (a1 ∪ b1)) = ((a0 ∪ a1) ∪ b1)
11	8, 10	lbtr 139	. . . . . . . 8 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ ((a0 ∪ a1) ∪ b1)
12	6, 11	letr 137	. . . . . . 7 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ ((a0 ∪ a1) ∪ b1)
13	5, 12	bltr 138	. . . . . 6 (b0 ∩ (a0 ∪ p0)) ≤ ((a0 ∪ a1) ∪ b1)
14	2, 13	ler2an 173	. . . . 5 (b0 ∩ (a0 ∪ p0)) ≤ (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))
15		leor 159	. . . . . . 7 b1 ≤ ((b0 ∩ (a0 ∪ p0)) ∪ b1)
16	15	mldual2i 1127	. . . . . 6 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = ((((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) ∪ b1)
17		ancom 74	. . . . . . 7 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
18	17	ror 71	. . . . . 6 ((((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) ∪ b1) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
19	16, 18	tr 62	. . . . 5 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
20	14, 19	lbtr 139	. . . 4 (b0 ∩ (a0 ∪ p0)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
21	1	lelor 166	. . . 4 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
22	20, 21	letr 137	. . 3 (b0 ∩ (a0 ∪ p0)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
23		lea 160	. . . . . . . 8 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (a0 ∪ a1)
24		dp53lem.1	. . . . . . . . 9 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
25		dp53lem.2	. . . . . . . . 9 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
26	24, 25, 3	dp15 1162	. . . . . . . 8 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
27	23, 26	ler2an 173	. . . . . . 7 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))))
28		lear 161	. . . . . . . 8 (b1 ∩ (a0 ∪ a1)) ≤ (a0 ∪ a1)
29	28	mldual2i 1127	. . . . . . 7 ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
30	27, 29	lbtr 139	. . . . . 6 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
31		lea 160	. . . . . . 7 (b1 ∩ (a0 ∪ a1)) ≤ b1
32	31	lelor 166	. . . . . 6 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1))) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
33	30, 32	letr 137	. . . . 5 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
34		orcom 73	. . . . 5 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1) = (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
35	33, 34	lbtr 139	. . . 4 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
36		leid 148	. . . 4 (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
37	35, 36	lel2or 170	. . 3 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
38	22, 37	letr 137	. 2 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
39	1, 38	lel2or 170	1 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))

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:  dp53lemd  1166