Theorem oadp35lemc 1211

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

Hypotheses

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

Assertion

Ref	Expression
oadp35lemc	(b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))

Proof of Theorem oadp35lemc

Step	Hyp	Ref	Expression
1		or32 82	. . 3 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1)
2		orcom 73	. . 3 (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1) = (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))))
3		leo 158	. . . . . . . 8 a0 ≤ (a0 ∪ a1)
4		leo 158	. . . . . . . 8 b0 ≤ (b0 ∪ b1)
5	3, 4	le2an 169	. . . . . . 7 (a0 ∩ b0) ≤ ((a0 ∪ a1) ∩ (b0 ∪ b1))
6		oadp35lem.3	. . . . . . . 8 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
7	6	cm 61	. . . . . . 7 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = c2
8	5, 7	lbtr 139	. . . . . 6 (a0 ∩ b0) ≤ c2
9		leo 158	. . . . . . . . 9 a0 ≤ (a0 ∪ a2)
10		leo 158	. . . . . . . . 9 b0 ≤ (b0 ∪ b2)
11	9, 10	le2an 169	. . . . . . . 8 (a0 ∩ b0) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
12		oadp35lem.2	. . . . . . . . 9 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
13	12	cm 61	. . . . . . . 8 ((a0 ∪ a2) ∩ (b0 ∪ b2)) = c1
14	11, 13	lbtr 139	. . . . . . 7 (a0 ∩ b0) ≤ c1
15	14	lerr 150	. . . . . 6 (a0 ∩ b0) ≤ (c0 ∪ c1)
16	8, 15	ler2an 173	. . . . 5 (a0 ∩ b0) ≤ (c2 ∩ (c0 ∪ c1))
17	16	df-le2 131	. . . 4 ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) = (c2 ∩ (c0 ∪ c1))
18	17	lor 70	. . 3 (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1)))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
19	1, 2, 18	3tr 65	. 2 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
20	19	lan 77	1 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))

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

This theorem was proved from 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

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: (None)