Theorem dp15leme 1158

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

Hypotheses

Ref	Expression
dp15lema.1	d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
dp15lema.2	p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
dp15lema.3	e = (b0 ∩ (a0 ∪ p0))

Assertion

Ref	Expression
dp15leme	(((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))

Proof of Theorem dp15leme

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . 7 (a1 ∪ a2) = (a2 ∪ a1)
2		ax-a2 31	. . . . . . . 8 (a1 ∪ b1) = (b1 ∪ a1)
3	2	lan 77	. . . . . . 7 (a0 ∩ (a1 ∪ b1)) = (a0 ∩ (b1 ∪ a1))
4	1, 3	2or 72	. . . . . 6 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1)))
5		orass 75	. . . . . 6 ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
6	4, 5	tr 62	. . . . 5 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
7		ml3le 1129	. . . . . 6 (a1 ∪ (a0 ∩ (b1 ∪ a1))) ≤ (a1 ∪ (b1 ∩ (a0 ∪ a1)))
8	7	lelor 166	. . . . 5 (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1)))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
9	6, 8	bltr 138	. . . 4 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
10		orass 75	. . . . . 6 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
11	10	cm 61	. . . . 5 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
12		ax-a2 31	. . . . . 6 (a2 ∪ a1) = (a1 ∪ a2)
13	12	ror 71	. . . . 5 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
14	11, 13	tr 62	. . . 4 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
15	9, 14	lbtr 139	. . 3 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
16	15	leran 153	. 2 (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)) ≤ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))
17	16	lelor 166	1 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7

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

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

This theorem is used by:  dp15lemh  1161