Theorem xdp53 1200

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

Hypotheses

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

Assertion

Ref	Expression
xdp53	p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))

Proof of Theorem xdp53

Step	Hyp	Ref	Expression
1		leor 159	. 2 p ≤ (a0 ∪ p)
2		leo 158	. . 3 a0 ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3		xdp53.5	. . . . . . . 8 p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
4		anass 76	. . . . . . . 8 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2)) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
5	3, 4	tr 62	. . . . . . 7 p = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
6		xdp53.4	. . . . . . . . . . 11 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
7	6	lan 77	. . . . . . . . . 10 ((a0 ∪ b0) ∩ p0) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
8	7	cm 61	. . . . . . . . 9 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = ((a0 ∪ b0) ∩ p0)
9		leao4 165	. . . . . . . . 9 ((a0 ∪ b0) ∩ p0) ≤ (a0 ∪ p0)
10	8, 9	bltr 138	. . . . . . . 8 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (a0 ∪ p0)
11		lea 160	. . . . . . . . 9 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (a0 ∪ b0)
12		orcom 73	. . . . . . . . 9 (a0 ∪ b0) = (b0 ∪ a0)
13	11, 12	lbtr 139	. . . . . . . 8 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (b0 ∪ a0)
14	10, 13	ler2an 173	. . . . . . 7 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ ((a0 ∪ p0) ∩ (b0 ∪ a0))
15	5, 14	bltr 138	. . . . . 6 p ≤ ((a0 ∪ p0) ∩ (b0 ∪ a0))
16		leo 158	. . . . . . . 8 a0 ≤ (a0 ∪ p0)
17	16	mldual2i 1127	. . . . . . 7 ((a0 ∪ p0) ∩ (b0 ∪ a0)) = (((a0 ∪ p0) ∩ b0) ∪ a0)
18		ancom 74	. . . . . . . 8 ((a0 ∪ p0) ∩ b0) = (b0 ∩ (a0 ∪ p0))
19	18	ror 71	. . . . . . 7 (((a0 ∪ p0) ∩ b0) ∪ a0) = ((b0 ∩ (a0 ∪ p0)) ∪ a0)
20	17, 19	tr 62	. . . . . 6 ((a0 ∪ p0) ∩ (b0 ∪ a0)) = ((b0 ∩ (a0 ∪ p0)) ∪ a0)
21	15, 20	lbtr 139	. . . . 5 p ≤ ((b0 ∩ (a0 ∪ p0)) ∪ a0)
22	2	lelor 166	. . . . 5 ((b0 ∩ (a0 ∪ p0)) ∪ a0) ≤ ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))))
23	21, 22	letr 137	. . . 4 p ≤ ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))))
24		lea 160	. . . . . . . 8 (b0 ∩ (a0 ∪ p0)) ≤ b0
25		leor 159	. . . . . . . . 9 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ (b0 ∩ (a0 ∪ p0)))
26		leo 158	. . . . . . . . . 10 b1 ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
27		leo 158	. . . . . . . . . . . . . 14 (b0 ∩ (a0 ∪ p0)) ≤ ((b0 ∩ (a0 ∪ p0)) ∪ b1)
28	6	lor 70	. . . . . . . . . . . . . . . 16 (a0 ∪ p0) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
29	28	lan 77	. . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ p0)) = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
30		lear 161	. . . . . . . . . . . . . . . 16 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
31		lea 160	. . . . . . . . . . . . . . . . . 18 ((a1 ∪ b1) ∩ (a2 ∪ b2)) ≤ (a1 ∪ b1)
32	31	lelor 166	. . . . . . . . . . . . . . . . 17 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (a0 ∪ (a1 ∪ b1))
33		ax-a3 32	. . . . . . . . . . . . . . . . . 18 ((a0 ∪ a1) ∪ b1) = (a0 ∪ (a1 ∪ b1))
34	33	cm 61	. . . . . . . . . . . . . . . . 17 (a0 ∪ (a1 ∪ b1)) = ((a0 ∪ a1) ∪ b1)
35	32, 34	lbtr 139	. . . . . . . . . . . . . . . 16 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ ((a0 ∪ a1) ∪ b1)
36	30, 35	letr 137	. . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ ((a0 ∪ a1) ∪ b1)
37	29, 36	bltr 138	. . . . . . . . . . . . . 14 (b0 ∩ (a0 ∪ p0)) ≤ ((a0 ∪ a1) ∪ b1)
38	27, 37	ler2an 173	. . . . . . . . . . . . 13 (b0 ∩ (a0 ∪ p0)) ≤ (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))
39		leor 159	. . . . . . . . . . . . . . 15 b1 ≤ ((b0 ∩ (a0 ∪ p0)) ∪ b1)
40	39	mldual2i 1127	. . . . . . . . . . . . . 14 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = ((((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) ∪ b1)
41		ancom 74	. . . . . . . . . . . . . . 15 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
42	41	ror 71	. . . . . . . . . . . . . 14 ((((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) ∪ b1) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
43	40, 42	tr 62	. . . . . . . . . . . . 13 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
44	38, 43	lbtr 139	. . . . . . . . . . . 12 (b0 ∩ (a0 ∪ p0)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
45	26	lelor 166	. . . . . . . . . . . 12 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
46	44, 45	letr 137	. . . . . . . . . . 11 (b0 ∩ (a0 ∪ p0)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
47		lea 160	. . . . . . . . . . . . . . . 16 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (a0 ∪ a1)
48		xdp53.1	. . . . . . . . . . . . . . . . 17 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
49		xdp53.2	. . . . . . . . . . . . . . . . 17 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
50	48, 49, 6	dp15 1162	. . . . . . . . . . . . . . . 16 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
51	47, 50	ler2an 173	. . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))))
52		lear 161	. . . . . . . . . . . . . . . 16 (b1 ∩ (a0 ∪ a1)) ≤ (a0 ∪ a1)
53	52	mldual2i 1127	. . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
54	51, 53	lbtr 139	. . . . . . . . . . . . . 14 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
55		lea 160	. . . . . . . . . . . . . . 15 (b1 ∩ (a0 ∪ a1)) ≤ b1
56	55	lelor 166	. . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1))) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
57	54, 56	letr 137	. . . . . . . . . . . . 13 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
58		orcom 73	. . . . . . . . . . . . 13 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1) = (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
59	57, 58	lbtr 139	. . . . . . . . . . . 12 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
60		leid 148	. . . . . . . . . . . 12 (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
61	59, 60	lel2or 170	. . . . . . . . . . 11 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
62	46, 61	letr 137	. . . . . . . . . 10 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
63	26, 62	lel2or 170	. . . . . . . . 9 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
64	25, 63	letr 137	. . . . . . . 8 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
65	24, 64	ler2an 173	. . . . . . 7 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
66		or32 82	. . . . . . . . . . 11 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1)
67		orcom 73	. . . . . . . . . . 11 (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1) = (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))))
68		leo 158	. . . . . . . . . . . . . . . 16 a0 ≤ (a0 ∪ a1)
69		leo 158	. . . . . . . . . . . . . . . 16 b0 ≤ (b0 ∪ b1)
70	68, 69	le2an 169	. . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ ((a0 ∪ a1) ∩ (b0 ∪ b1))
71		xdp53.3	. . . . . . . . . . . . . . . 16 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
72	71	cm 61	. . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = c2
73	70, 72	lbtr 139	. . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ c2
74		leo 158	. . . . . . . . . . . . . . . . 17 a0 ≤ (a0 ∪ a2)
75		leo 158	. . . . . . . . . . . . . . . . 17 b0 ≤ (b0 ∪ b2)
76	74, 75	le2an 169	. . . . . . . . . . . . . . . 16 (a0 ∩ b0) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
77	49	cm 61	. . . . . . . . . . . . . . . 16 ((a0 ∪ a2) ∩ (b0 ∪ b2)) = c1
78	76, 77	lbtr 139	. . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ c1
79	78	lerr 150	. . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ (c0 ∪ c1)
80	73, 79	ler2an 173	. . . . . . . . . . . . 13 (a0 ∩ b0) ≤ (c2 ∩ (c0 ∪ c1))
81	80	df-le2 131	. . . . . . . . . . . 12 ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) = (c2 ∩ (c0 ∪ c1))
82	81	lor 70	. . . . . . . . . . 11 (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1)))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
83	66, 67, 82	3tr 65	. . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
84	83	lan 77	. . . . . . . . 9 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
85	71	ran 78	. . . . . . . . . . . . . 14 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1))
86		an32 83	. . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
87	85, 86	tr 62	. . . . . . . . . . . . 13 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
88	87	lor 70	. . . . . . . . . . . 12 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1)))
89		leor 159	. . . . . . . . . . . . 13 b1 ≤ (b0 ∪ b1)
90	89	ml2i 1125	. . . . . . . . . . . 12 (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))) = ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1))
91		ancom 74	. . . . . . . . . . . 12 ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1)) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
92	88, 90, 91	3tr 65	. . . . . . . . . . 11 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
93	92	lan 77	. . . . . . . . . 10 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
94		anass 76	. . . . . . . . . . 11 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
95	94	cm 61	. . . . . . . . . 10 (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))) = ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
96		anabs 121	. . . . . . . . . . 11 (b0 ∩ (b0 ∪ b1)) = b0
97	96	ran 78	. . . . . . . . . 10 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
98	93, 95, 97	3tr 65	. . . . . . . . 9 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
99	84, 98	tr 62	. . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
100	99	cm 61	. . . . . . 7 (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
101	65, 100	lbtr 139	. . . . . 6 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
102		orass 75	. . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
103		orcom 73	. . . . . . . . . 10 ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
104	102, 103	tr 62	. . . . . . . . 9 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
105	104	lan 77	. . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0)))
106		lear 161	. . . . . . . . 9 (a0 ∩ b0) ≤ b0
107	106	mldual2i 1127	. . . . . . . 8 (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))) = ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0))
108		orcom 73	. . . . . . . 8 ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0)) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
109	105, 107, 108	3tr 65	. . . . . . 7 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
110		lea 160	. . . . . . . 8 (a0 ∩ b0) ≤ a0
111	110	leror 152	. . . . . . 7 ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
112	109, 111	bltr 138	. . . . . 6 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
113	101, 112	letr 137	. . . . 5 (b0 ∩ (a0 ∪ p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
114	113	df-le2 131	. . . 4 ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))) = (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
115	23, 114	lbtr 139	. . 3 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
116	2, 115	lel2or 170	. 2 (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
117	1, 116	letr 137	1 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (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)