Theorem dp15lemc 1156

Description: Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 10-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
dp15lemc	((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))

Proof of Theorem dp15lemc

Step	Hyp	Ref	Expression
1		dp15lema.1	. . 3 d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
2		dp15lema.2	. . 3 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
3		dp15lema.3	. . 3 e = (b0 ∩ (a0 ∪ p0))
4	1, 2, 3	dp15lemb 1155	. 2 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
5	3	ror 71	. . 3 (e ∪ b1) = ((b0 ∩ (a0 ∪ p0)) ∪ b1)
6	5	lan 77	. 2 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
7	1	lor 70	. . . 4 (a0 ∪ d) = (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
8	3	ror 71	. . . 4 (e ∪ b2) = ((b0 ∩ (a0 ∪ p0)) ∪ b2)
9	7, 8	2an 79	. . 3 ((a0 ∪ d) ∩ (e ∪ b2)) = ((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2))
10	1	lor 70	. . . 4 (a1 ∪ d) = (a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
11	10	ran 78	. . 3 ((a1 ∪ d) ∩ (b1 ∪ b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))
12	9, 11	2or 72	. 2 (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) = (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
13	4, 6, 12	le3tr2 141	1 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (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-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122  ax-arg 1153

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