Theorem xxdp41 1201

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

Hypotheses

Ref	Expression
xxdp.1	p2 ≤ (a2 ∪ b2)
xxdp.c0	c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
xxdp.c1	c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
xxdp.c2	c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
xxdp.d	d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
xxdp.e	e = (b0 ∩ (a0 ∪ p0))
xxdp.p	p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
xxdp.p0	p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
xxdp.p2	p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))

Assertion

Ref	Expression
xxdp41	c2 ≤ (c0 ∪ c1)

Proof of Theorem xxdp41

Step	Hyp	Ref	Expression
1		xxdp.c2	. . . . . . . . . . . 12 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
2		ancom 74	. . . . . . . . . . . 12 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = ((b0 ∪ b1) ∩ (a0 ∪ a1))
3	1, 2	tr 62	. . . . . . . . . . 11 c2 = ((b0 ∪ b1) ∩ (a0 ∪ a1))
4		leor 159	. . . . . . . . . . . . 13 b0 ≤ (a0 ∪ b0)
5	4	leror 152	. . . . . . . . . . . 12 (b0 ∪ b1) ≤ ((a0 ∪ b0) ∪ b1)
6		leo 158	. . . . . . . . . . . 12 (a0 ∪ a1) ≤ ((a0 ∪ a1) ∪ b1)
7	5, 6	le2an 169	. . . . . . . . . . 11 ((b0 ∪ b1) ∩ (a0 ∪ a1)) ≤ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))
8	3, 7	bltr 138	. . . . . . . . . 10 c2 ≤ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))
9	8	df2le2 136	. . . . . . . . 9 (c2 ∩ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))) = c2
10	9	cm 61	. . . . . . . 8 c2 = (c2 ∩ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)))
11		anass 76	. . . . . . . . 9 ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1)) = (c2 ∩ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)))
12	11	cm 61	. . . . . . . 8 (c2 ∩ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))) = ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1))
13	10, 12	tr 62	. . . . . . 7 c2 = ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1))
14		ax-a2 31	. . . . . . . . . . . . . . . 16 (a0 ∪ a1) = (a1 ∪ a0)
15	14	ror 71	. . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∪ b1) = ((a1 ∪ a0) ∪ b1)
16		or32 82	. . . . . . . . . . . . . . 15 ((a1 ∪ a0) ∪ b1) = ((a1 ∪ b1) ∪ a0)
17	15, 16	tr 62	. . . . . . . . . . . . . 14 ((a0 ∪ a1) ∪ b1) = ((a1 ∪ b1) ∪ a0)
18	17	lan 77	. . . . . . . . . . . . 13 (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = (((a0 ∪ b0) ∪ b1) ∩ ((a1 ∪ b1) ∪ a0))
19		ancom 74	. . . . . . . . . . . . 13 (((a0 ∪ b0) ∪ b1) ∩ ((a1 ∪ b1) ∪ a0)) = (((a1 ∪ b1) ∪ a0) ∩ ((a0 ∪ b0) ∪ b1))
20	18, 19	tr 62	. . . . . . . . . . . 12 (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = (((a1 ∪ b1) ∪ a0) ∩ ((a0 ∪ b0) ∪ b1))
21		leor 159	. . . . . . . . . . . . . 14 b1 ≤ (a1 ∪ b1)
22	21	ler 149	. . . . . . . . . . . . 13 b1 ≤ ((a1 ∪ b1) ∪ a0)
23	22	mldual2i 1127	. . . . . . . . . . . 12 (((a1 ∪ b1) ∪ a0) ∩ ((a0 ∪ b0) ∪ b1)) = ((((a1 ∪ b1) ∪ a0) ∩ (a0 ∪ b0)) ∪ b1)
24		ancom 74	. . . . . . . . . . . . . 14 (((a1 ∪ b1) ∪ a0) ∩ (a0 ∪ b0)) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∪ a0))
25		leo 158	. . . . . . . . . . . . . . 15 a0 ≤ (a0 ∪ b0)
26	25	mldual2i 1127	. . . . . . . . . . . . . 14 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∪ a0)) = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ a0)
27	24, 26	tr 62	. . . . . . . . . . . . 13 (((a1 ∪ b1) ∪ a0) ∩ (a0 ∪ b0)) = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ a0)
28	27	ror 71	. . . . . . . . . . . 12 ((((a1 ∪ b1) ∪ a0) ∩ (a0 ∪ b0)) ∪ b1) = ((((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ a0) ∪ b1)
29	20, 23, 28	3tr 65	. . . . . . . . . . 11 (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = ((((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ a0) ∪ b1)
30		orass 75	. . . . . . . . . . 11 ((((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ a0) ∪ b1) = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ (a0 ∪ b1))
31		orcom 73	. . . . . . . . . . 11 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∪ (a0 ∪ b1)) = ((a0 ∪ b1) ∪ ((a0 ∪ b0) ∩ (a1 ∪ b1)))
32	29, 30, 31	3tr 65	. . . . . . . . . 10 (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = ((a0 ∪ b1) ∪ ((a0 ∪ b0) ∩ (a1 ∪ b1)))
33		leo 158	. . . . . . . . . . 11 (a0 ∪ b1) ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
34		xxdp.p2	. . . . . . . . . . . . . . . . 17 p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))
35	34	cm 61	. . . . . . . . . . . . . . . 16 ((a0 ∪ b0) ∩ (a1 ∪ b1)) = p2
36		xxdp.1	. . . . . . . . . . . . . . . 16 p2 ≤ (a2 ∪ b2)
37	35, 36	bltr 138	. . . . . . . . . . . . . . 15 ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)
38	37	df2le2 136	. . . . . . . . . . . . . 14 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2)) = ((a0 ∪ b0) ∩ (a1 ∪ b1))
39	38	cm 61	. . . . . . . . . . . . 13 ((a0 ∪ b0) ∩ (a1 ∪ b1)) = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
40		xxdp.p	. . . . . . . . . . . . . 14 p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
41	40	cm 61	. . . . . . . . . . . . 13 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2)) = p
42	39, 41	tr 62	. . . . . . . . . . . 12 ((a0 ∪ b0) ∩ (a1 ∪ b1)) = p
43		xxdp.c0	. . . . . . . . . . . . 13 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
44		xxdp.c1	. . . . . . . . . . . . 13 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
45	43, 44, 1, 40	dp34 1181	. . . . . . . . . . . 12 p ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
46	42, 45	bltr 138	. . . . . . . . . . 11 ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
47	33, 46	lel2or 170	. . . . . . . . . 10 ((a0 ∪ b1) ∪ ((a0 ∪ b0) ∩ (a1 ∪ b1))) ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
48	32, 47	bltr 138	. . . . . . . . 9 (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) ≤ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))
49	48	lelan 167	. . . . . . . 8 (c2 ∩ (((a0 ∪ b0) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))) ≤ (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
50	11, 49	bltr 138	. . . . . . 7 ((c2 ∩ ((a0 ∪ b0) ∪ b1)) ∩ ((a0 ∪ a1) ∪ b1)) ≤ (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
51	13, 50	bltr 138	. . . . . 6 c2 ≤ (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
52		mldual 1124	. . . . . . 7 (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = ((c2 ∩ (a0 ∪ b1)) ∪ (c2 ∩ (c0 ∪ c1)))
53		ancom 74	. . . . . . . 8 (c2 ∩ (c0 ∪ c1)) = ((c0 ∪ c1) ∩ c2)
54	53	lor 70	. . . . . . 7 ((c2 ∩ (a0 ∪ b1)) ∪ (c2 ∩ (c0 ∪ c1))) = ((c2 ∩ (a0 ∪ b1)) ∪ ((c0 ∪ c1) ∩ c2))
55		lea 160	. . . . . . . . 9 (c2 ∩ (a0 ∪ b1)) ≤ c2
56	55	ml2i 1125	. . . . . . . 8 ((c2 ∩ (a0 ∪ b1)) ∪ ((c0 ∪ c1) ∩ c2)) = (((c2 ∩ (a0 ∪ b1)) ∪ (c0 ∪ c1)) ∩ c2)
57		ancom 74	. . . . . . . 8 (((c2 ∩ (a0 ∪ b1)) ∪ (c0 ∪ c1)) ∩ c2) = (c2 ∩ ((c2 ∩ (a0 ∪ b1)) ∪ (c0 ∪ c1)))
58		ax-a2 31	. . . . . . . . 9 ((c2 ∩ (a0 ∪ b1)) ∪ (c0 ∪ c1)) = ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1)))
59	58	lan 77	. . . . . . . 8 (c2 ∩ ((c2 ∩ (a0 ∪ b1)) ∪ (c0 ∪ c1))) = (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1))))
60	56, 57, 59	3tr 65	. . . . . . 7 ((c2 ∩ (a0 ∪ b1)) ∪ ((c0 ∪ c1) ∩ c2)) = (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1))))
61	52, 54, 60	3tr 65	. . . . . 6 (c2 ∩ ((a0 ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1))))
62	51, 61	lbtr 139	. . . . 5 c2 ≤ (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1))))
63		mldual 1124	. . . . . . 7 (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1)))) = ((c2 ∩ (c0 ∪ c1)) ∪ (c2 ∩ (a0 ∪ b1)))
64	1	ran 78	. . . . . . . . 9 (c2 ∩ (a0 ∪ b1)) = (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (a0 ∪ b1))
65		anass 76	. . . . . . . . 9 (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (a0 ∪ b1)) = ((a0 ∪ a1) ∩ ((b0 ∪ b1) ∩ (a0 ∪ b1)))
66		leor 159	. . . . . . . . . . . . 13 b1 ≤ (b0 ∪ b1)
67	66	mldual2i 1127	. . . . . . . . . . . 12 ((b0 ∪ b1) ∩ (a0 ∪ b1)) = (((b0 ∪ b1) ∩ a0) ∪ b1)
68		orcom 73	. . . . . . . . . . . 12 (((b0 ∪ b1) ∩ a0) ∪ b1) = (b1 ∪ ((b0 ∪ b1) ∩ a0))
69		ancom 74	. . . . . . . . . . . . 13 ((b0 ∪ b1) ∩ a0) = (a0 ∩ (b0 ∪ b1))
70	69	lor 70	. . . . . . . . . . . 12 (b1 ∪ ((b0 ∪ b1) ∩ a0)) = (b1 ∪ (a0 ∩ (b0 ∪ b1)))
71	67, 68, 70	3tr 65	. . . . . . . . . . 11 ((b0 ∪ b1) ∩ (a0 ∪ b1)) = (b1 ∪ (a0 ∩ (b0 ∪ b1)))
72	71	lan 77	. . . . . . . . . 10 ((a0 ∪ a1) ∩ ((b0 ∪ b1) ∩ (a0 ∪ b1))) = ((a0 ∪ a1) ∩ (b1 ∪ (a0 ∩ (b0 ∪ b1))))
73		leao1 162	. . . . . . . . . . 11 (a0 ∩ (b0 ∪ b1)) ≤ (a0 ∪ a1)
74	73	mldual2i 1127	. . . . . . . . . 10 ((a0 ∪ a1) ∩ (b1 ∪ (a0 ∩ (b0 ∪ b1)))) = (((a0 ∪ a1) ∩ b1) ∪ (a0 ∩ (b0 ∪ b1)))
75		orcom 73	. . . . . . . . . . 11 (((a0 ∪ a1) ∩ b1) ∪ (a0 ∩ (b0 ∪ b1))) = ((a0 ∩ (b0 ∪ b1)) ∪ ((a0 ∪ a1) ∩ b1))
76		ancom 74	. . . . . . . . . . . 12 ((a0 ∪ a1) ∩ b1) = (b1 ∩ (a0 ∪ a1))
77	76	lor 70	. . . . . . . . . . 11 ((a0 ∩ (b0 ∪ b1)) ∪ ((a0 ∪ a1) ∩ b1)) = ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
78	75, 77	tr 62	. . . . . . . . . 10 (((a0 ∪ a1) ∩ b1) ∪ (a0 ∩ (b0 ∪ b1))) = ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
79	72, 74, 78	3tr 65	. . . . . . . . 9 ((a0 ∪ a1) ∩ ((b0 ∪ b1) ∩ (a0 ∪ b1))) = ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
80	64, 65, 79	3tr 65	. . . . . . . 8 (c2 ∩ (a0 ∪ b1)) = ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
81	80	lor 70	. . . . . . 7 ((c2 ∩ (c0 ∪ c1)) ∪ (c2 ∩ (a0 ∪ b1))) = ((c2 ∩ (c0 ∪ c1)) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
82	63, 81	tr 62	. . . . . 6 (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1)))) = ((c2 ∩ (c0 ∪ c1)) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
83		lear 161	. . . . . . 7 (c2 ∩ (c0 ∪ c1)) ≤ (c0 ∪ c1)
84	83	leror 152	. . . . . 6 ((c2 ∩ (c0 ∪ c1)) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) ≤ ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
85	82, 84	bltr 138	. . . . 5 (c2 ∩ ((c0 ∪ c1) ∪ (c2 ∩ (a0 ∪ b1)))) ≤ ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
86	62, 85	letr 137	. . . 4 c2 ≤ ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
87		orcom 73	. . . . . . 7 ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))) = ((b1 ∩ (a0 ∪ a1)) ∪ (a0 ∩ (b0 ∪ b1)))
88	87	lor 70	. . . . . 6 ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ ((b1 ∩ (a0 ∪ a1)) ∪ (a0 ∩ (b0 ∪ b1))))
89		or4 84	. . . . . . 7 ((c0 ∪ c1) ∪ ((b1 ∩ (a0 ∪ a1)) ∪ (a0 ∩ (b0 ∪ b1)))) = ((c0 ∪ (b1 ∩ (a0 ∪ a1))) ∪ (c1 ∪ (a0 ∩ (b0 ∪ b1))))
90		ancom 74	. . . . . . . . . 10 ((a1 ∪ a2) ∩ (b1 ∪ b2)) = ((b1 ∪ b2) ∩ (a1 ∪ a2))
91	43, 90	tr 62	. . . . . . . . 9 c0 = ((b1 ∪ b2) ∩ (a1 ∪ a2))
92	91	ror 71	. . . . . . . 8 (c0 ∪ (b1 ∩ (a0 ∪ a1))) = (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1)))
93	44	ror 71	. . . . . . . 8 (c1 ∪ (a0 ∩ (b0 ∪ b1))) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a0 ∩ (b0 ∪ b1)))
94	92, 93	2or 72	. . . . . . 7 ((c0 ∪ (b1 ∩ (a0 ∪ a1))) ∪ (c1 ∪ (a0 ∩ (b0 ∪ b1)))) = ((((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a0 ∩ (b0 ∪ b1))))
95	89, 94	tr 62	. . . . . 6 ((c0 ∪ c1) ∪ ((b1 ∩ (a0 ∪ a1)) ∪ (a0 ∩ (b0 ∪ b1)))) = ((((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a0 ∩ (b0 ∪ b1))))
96		leao1 162	. . . . . . . 8 (b1 ∩ (a0 ∪ a1)) ≤ (b1 ∪ b2)
97	96	mli 1126	. . . . . . 7 (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) = ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))))
98		leao1 162	. . . . . . . 8 (a0 ∩ (b0 ∪ b1)) ≤ (a0 ∪ a2)
99	98	mli 1126	. . . . . . 7 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a0 ∩ (b0 ∪ b1))) = ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1))))
100	97, 99	2or 72	. . . . . 6 ((((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a0 ∩ (b0 ∪ b1)))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1)))))
101	88, 95, 100	3tr 65	. . . . 5 ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1)))))
102		or32 82	. . . . . . . 8 ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ (b1 ∩ (a0 ∪ a1))) ∪ a2)
103		ml3 1130	. . . . . . . . . 10 (a1 ∪ (b1 ∩ (a0 ∪ a1))) = (a1 ∪ (a0 ∩ (b1 ∪ a1)))
104		orcom 73	. . . . . . . . . . . 12 (b1 ∪ a1) = (a1 ∪ b1)
105	104	lan 77	. . . . . . . . . . 11 (a0 ∩ (b1 ∪ a1)) = (a0 ∩ (a1 ∪ b1))
106	105	lor 70	. . . . . . . . . 10 (a1 ∪ (a0 ∩ (b1 ∪ a1))) = (a1 ∪ (a0 ∩ (a1 ∪ b1)))
107	103, 106	tr 62	. . . . . . . . 9 (a1 ∪ (b1 ∩ (a0 ∪ a1))) = (a1 ∪ (a0 ∩ (a1 ∪ b1)))
108	107	ror 71	. . . . . . . 8 ((a1 ∪ (b1 ∩ (a0 ∪ a1))) ∪ a2) = ((a1 ∪ (a0 ∩ (a1 ∪ b1))) ∪ a2)
109		or32 82	. . . . . . . 8 ((a1 ∪ (a0 ∩ (a1 ∪ b1))) ∪ a2) = ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))
110	102, 108, 109	3tr 65	. . . . . . 7 ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))
111	110	lan 77	. . . . . 6 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) = ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))))
112		or32 82	. . . . . . . 8 ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1))) = ((b0 ∪ (a0 ∩ (b0 ∪ b1))) ∪ b2)
113		orcom 73	. . . . . . . . . . . 12 (b0 ∪ b1) = (b1 ∪ b0)
114	113	lan 77	. . . . . . . . . . 11 (a0 ∩ (b0 ∪ b1)) = (a0 ∩ (b1 ∪ b0))
115	114	lor 70	. . . . . . . . . 10 (b0 ∪ (a0 ∩ (b0 ∪ b1))) = (b0 ∪ (a0 ∩ (b1 ∪ b0)))
116		ml3 1130	. . . . . . . . . 10 (b0 ∪ (a0 ∩ (b1 ∪ b0))) = (b0 ∪ (b1 ∩ (a0 ∪ b0)))
117	115, 116	tr 62	. . . . . . . . 9 (b0 ∪ (a0 ∩ (b0 ∪ b1))) = (b0 ∪ (b1 ∩ (a0 ∪ b0)))
118	117	ror 71	. . . . . . . 8 ((b0 ∪ (a0 ∩ (b0 ∪ b1))) ∪ b2) = ((b0 ∪ (b1 ∩ (a0 ∪ b0))) ∪ b2)
119		or32 82	. . . . . . . 8 ((b0 ∪ (b1 ∩ (a0 ∪ b0))) ∪ b2) = ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))
120	112, 118, 119	3tr 65	. . . . . . 7 ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1))) = ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))
121	120	lan 77	. . . . . 6 ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1)))) = ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0))))
122	111, 121	2or 72	. . . . 5 (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a0 ∩ (b0 ∪ b1))))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))))
123	101, 122	tr 62	. . . 4 ((c0 ∪ c1) ∪ ((a0 ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))))
124	86, 123	lbtr 139	. . 3 c2 ≤ (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))))
125		lea 160	. . . . . . 7 (a0 ∩ (a1 ∪ b1)) ≤ a0
126	25	leran 153	. . . . . . . 8 (a0 ∩ (a1 ∪ b1)) ≤ ((a0 ∪ b0) ∩ (a1 ∪ b1))
127	126, 37	letr 137	. . . . . . 7 (a0 ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2)
128	125, 127	ler2an 173	. . . . . 6 (a0 ∩ (a1 ∪ b1)) ≤ (a0 ∩ (a2 ∪ b2))
129	128	lelor 166	. . . . 5 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))
130	129	lelan 167	. . . 4 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ≤ ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2))))
131		lea 160	. . . . . . 7 (b1 ∩ (a0 ∪ b0)) ≤ b1
132		lear 161	. . . . . . . . 9 (b1 ∩ (a0 ∪ b0)) ≤ (a0 ∪ b0)
133		leao3 164	. . . . . . . . 9 (b1 ∩ (a0 ∪ b0)) ≤ (a1 ∪ b1)
134	132, 133	ler2an 173	. . . . . . . 8 (b1 ∩ (a0 ∪ b0)) ≤ ((a0 ∪ b0) ∩ (a1 ∪ b1))
135	134, 37	letr 137	. . . . . . 7 (b1 ∩ (a0 ∪ b0)) ≤ (a2 ∪ b2)
136	131, 135	ler2an 173	. . . . . 6 (b1 ∩ (a0 ∪ b0)) ≤ (b1 ∩ (a2 ∪ b2))
137	136	lelor 166	. . . . 5 ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0))) ≤ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2)))
138	137	lelan 167	. . . 4 ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0)))) ≤ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))))
139	130, 138	le2or 168	. . 3 (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a0 ∪ b0))))) ≤ (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2)))))
140	124, 139	letr 137	. 2 c2 ≤ (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2)))))
141		ax-a2 31	. . . . . . . . . 10 (a2 ∪ b2) = (b2 ∪ a2)
142	141	lan 77	. . . . . . . . 9 (a0 ∩ (a2 ∪ b2)) = (a0 ∩ (b2 ∪ a2))
143	142	lor 70	. . . . . . . 8 (a2 ∪ (a0 ∩ (a2 ∪ b2))) = (a2 ∪ (a0 ∩ (b2 ∪ a2)))
144		ml3 1130	. . . . . . . 8 (a2 ∪ (a0 ∩ (b2 ∪ a2))) = (a2 ∪ (b2 ∩ (a0 ∪ a2)))
145	143, 144	tr 62	. . . . . . 7 (a2 ∪ (a0 ∩ (a2 ∪ b2))) = (a2 ∪ (b2 ∩ (a0 ∪ a2)))
146	145	lor 70	. . . . . 6 (a1 ∪ (a2 ∪ (a0 ∩ (a2 ∪ b2)))) = (a1 ∪ (a2 ∪ (b2 ∩ (a0 ∪ a2))))
147		orass 75	. . . . . 6 ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2))) = (a1 ∪ (a2 ∪ (a0 ∩ (a2 ∪ b2))))
148		orass 75	. . . . . 6 ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2))) = (a1 ∪ (a2 ∪ (b2 ∩ (a0 ∪ a2))))
149	146, 147, 148	3tr1 63	. . . . 5 ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2))) = ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))
150	149	lan 77	. . . 4 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) = ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2))))
151		ml3 1130	. . . . . . 7 (b2 ∪ (b1 ∩ (a2 ∪ b2))) = (b2 ∪ (a2 ∩ (b1 ∪ b2)))
152	151	lor 70	. . . . . 6 (b0 ∪ (b2 ∪ (b1 ∩ (a2 ∪ b2)))) = (b0 ∪ (b2 ∪ (a2 ∩ (b1 ∪ b2))))
153		orass 75	. . . . . 6 ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))) = (b0 ∪ (b2 ∪ (b1 ∩ (a2 ∪ b2))))
154		orass 75	. . . . . 6 ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2))) = (b0 ∪ (b2 ∪ (a2 ∩ (b1 ∪ b2))))
155	152, 153, 154	3tr1 63	. . . . 5 ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))) = ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2)))
156	155	lan 77	. . . 4 ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2)))) = ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2))))
157	150, 156	2or 72	. . 3 (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))))) = (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2)))))
158		leao3 164	. . . . . 6 (b2 ∩ (a0 ∪ a2)) ≤ (b1 ∪ b2)
159	158	mldual2i 1127	. . . . 5 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) = (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b2 ∩ (a0 ∪ a2)))
160	91	ror 71	. . . . . 6 (c0 ∪ (b2 ∩ (a0 ∪ a2))) = (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b2 ∩ (a0 ∪ a2)))
161	160	cm 61	. . . . 5 (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b2 ∩ (a0 ∪ a2))) = (c0 ∪ (b2 ∩ (a0 ∪ a2)))
162	159, 161	tr 62	. . . 4 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) = (c0 ∪ (b2 ∩ (a0 ∪ a2)))
163		leao3 164	. . . . . 6 (a2 ∩ (b1 ∪ b2)) ≤ (a0 ∪ a2)
164	163	mldual2i 1127	. . . . 5 ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2)))) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a2 ∩ (b1 ∪ b2)))
165	44	ror 71	. . . . . 6 (c1 ∪ (a2 ∩ (b1 ∪ b2))) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a2 ∩ (b1 ∪ b2)))
166	165	cm 61	. . . . 5 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (a2 ∩ (b1 ∪ b2))) = (c1 ∪ (a2 ∩ (b1 ∪ b2)))
167	164, 166	tr 62	. . . 4 ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2)))) = (c1 ∪ (a2 ∩ (b1 ∪ b2)))
168	162, 167	2or 72	. . 3 (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b2 ∩ (a0 ∪ a2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (a2 ∩ (b1 ∪ b2))))) = ((c0 ∪ (b2 ∩ (a0 ∪ a2))) ∪ (c1 ∪ (a2 ∩ (b1 ∪ b2))))
169		or4 84	. . . 4 ((c0 ∪ (b2 ∩ (a0 ∪ a2))) ∪ (c1 ∪ (a2 ∩ (b1 ∪ b2)))) = ((c0 ∪ c1) ∪ ((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2))))
170		orcom 73	. . . 4 ((c0 ∪ c1) ∪ ((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2)))) = (((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2))) ∪ (c0 ∪ c1))
171		ancom 74	. . . . . . . 8 (b2 ∩ (a0 ∪ a2)) = ((a0 ∪ a2) ∩ b2)
172		leor 159	. . . . . . . . 9 b2 ≤ (b0 ∪ b2)
173	172	lelan 167	. . . . . . . 8 ((a0 ∪ a2) ∩ b2) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
174	171, 173	bltr 138	. . . . . . 7 (b2 ∩ (a0 ∪ a2)) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
175		leor 159	. . . . . . . 8 a2 ≤ (a1 ∪ a2)
176	175	leran 153	. . . . . . 7 (a2 ∩ (b1 ∪ b2)) ≤ ((a1 ∪ a2) ∩ (b1 ∪ b2))
177	174, 176	le2or 168	. . . . . 6 ((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
178	44, 43	2or 72	. . . . . . . 8 (c1 ∪ c0) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2)))
179	178	cm 61	. . . . . . 7 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2))) = (c1 ∪ c0)
180		orcom 73	. . . . . . 7 (c1 ∪ c0) = (c0 ∪ c1)
181	179, 180	tr 62	. . . . . 6 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2))) = (c0 ∪ c1)
182	177, 181	lbtr 139	. . . . 5 ((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2))) ≤ (c0 ∪ c1)
183	182	df-le2 131	. . . 4 (((b2 ∩ (a0 ∪ a2)) ∪ (a2 ∩ (b1 ∪ b2))) ∪ (c0 ∪ c1)) = (c0 ∪ c1)
184	169, 170, 183	3tr 65	. . 3 ((c0 ∪ (b2 ∩ (a0 ∪ a2))) ∪ (c1 ∪ (a2 ∩ (b1 ∪ b2)))) = (c0 ∪ c1)
185	157, 168, 184	3tr 65	. 2 (((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (a0 ∩ (a2 ∪ b2)))) ∪ ((a0 ∪ a2) ∩ ((b0 ∪ b2) ∪ (b1 ∩ (a2 ∪ b2))))) = (c0 ∪ c1)
186	140, 185	lbtr 139	1 c2 ≤ (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: (None)