QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3dp43 GIF version
Theorem 3dp43 1208
Description: "3OA" version of xdp43 1207. Changed a2 to a1 and b2 to b1. (Contributed by NM, 11-Apr-2012.)
Hypotheses
Ref Expression
3dp.c0 c0 = ((a1 ∪ a1) ∩ (b1 ∪ b1))
3dp.c1 c1 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
3dp.c2 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
3dp.d d = (a1 ∪ (a0 ∩ (a1 ∪ b1)))
3dp.e e = (b0 ∩ (a0 ∪ p0))
3dp.p p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a1 ∪ b1))
3dp.p0 p0 = ((a1 ∪ b1) ∩ (a1 ∪ b1))
3dp.p2 p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))
Assertion
Ref Expression
3dp43 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Proof of Theorem 3dp43
StepHypRef Expression
1 leor 159 . 2 p ≤ (a0 ∪ p)
2 leo 158 . . 3 a0 ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3 3dp.p . . . . . . . 8 p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a1 ∪ b1))
4 anass 76 . . . . . . . 8 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a1 ∪ b1)) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
53, 4tr 62 . . . . . . 7 p = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
6 3dp.p0 . . . . . . . . . . 11 p0 = ((a1 ∪ b1) ∩ (a1 ∪ b1))
76lan 77 . . . . . . . . . 10 ((a0 ∪ b0) ∩ p0) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
87cm 61 . . . . . . . . 9 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1))) = ((a0 ∪ b0) ∩ p0)
9 leao4 165 . . . . . . . . 9 ((a0 ∪ b0) ∩ p0) ≤ (a0 ∪ p0)
108, 9bltr 138 . . . . . . . 8 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ (a0 ∪ p0)
11 lea 160 . . . . . . . . 9 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ (a0 ∪ b0)
12 orcom 73 . . . . . . . . 9 (a0 ∪ b0) = (b0 ∪ a0)
1311, 12lbtr 139 . . . . . . . 8 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ (b0 ∪ a0)
1410, 13ler2an 173 . . . . . . 7 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ ((a0 ∪ p0) ∩ (b0 ∪ a0))
155, 14bltr 138 . . . . . 6 p ≤ ((a0 ∪ p0) ∩ (b0 ∪ a0))
16 leo 158 . . . . . . . 8 a0 ≤ (a0 ∪ p0)
1716mldual2i 1127 . . . . . . 7 ((a0 ∪ p0) ∩ (b0 ∪ a0)) = (((a0 ∪ p0) ∩ b0) ∪ a0)
18 ancom 74 . . . . . . . 8 ((a0 ∪ p0) ∩ b0) = (b0 ∩ (a0 ∪ p0))
1918ror 71 . . . . . . 7 (((a0 ∪ p0) ∩ b0) ∪ a0) = ((b0 ∩ (a0 ∪ p0)) ∪ a0)
2017, 19tr 62 . . . . . 6 ((a0 ∪ p0) ∩ (b0 ∪ a0)) = ((b0 ∩ (a0 ∪ p0)) ∪ a0)
2115, 20lbtr 139 . . . . 5 p ≤ ((b0 ∩ (a0 ∪ p0)) ∪ a0)
222lelor 166 . . . . 5 ((b0 ∩ (a0 ∪ p0)) ∪ a0) ≤ ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))))
2321, 22letr 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)
286lor 70 . . . . . . . . . . . . . . . 16 (a0 ∪ p0) = (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
2928lan 77 . . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ p0)) = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))
30 lear 161 . . . . . . . . . . . . . . . 16 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))) ≤ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
31 lea 160 . . . . . . . . . . . . . . . . . 18 ((a1 ∪ b1) ∩ (a1 ∪ b1)) ≤ (a1 ∪ b1)
3231lelor 166 . . . . . . . . . . . . . . . . 17 (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ (a0 ∪ (a1 ∪ b1))
33 ax-a3 32 . . . . . . . . . . . . . . . . . 18 ((a0 ∪ a1) ∪ b1) = (a0 ∪ (a1 ∪ b1))
3433cm 61 . . . . . . . . . . . . . . . . 17 (a0 ∪ (a1 ∪ b1)) = ((a0 ∪ a1) ∪ b1)
3532, 34lbtr 139 . . . . . . . . . . . . . . . 16 (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) ≤ ((a0 ∪ a1) ∪ b1)
3630, 35letr 137 . . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))) ≤ ((a0 ∪ a1) ∪ b1)
3729, 36bltr 138 . . . . . . . . . . . . . 14 (b0 ∩ (a0 ∪ p0)) ≤ ((a0 ∪ a1) ∪ b1)
3827, 37ler2an 173 . . . . . . . . . . . . 13 (b0 ∩ (a0 ∪ p0)) ≤ (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1))
39 leor 159 . . . . . . . . . . . . . . 15 b1 ≤ ((b0 ∩ (a0 ∪ p0)) ∪ b1)
4039mldual2i 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))
4241ror 71 . . . . . . . . . . . . . 14 ((((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ (a0 ∪ a1)) ∪ b1) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
4340, 42tr 62 . . . . . . . . . . . . 13 (((b0 ∩ (a0 ∪ p0)) ∪ b1) ∩ ((a0 ∪ a1) ∪ b1)) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
4438, 43lbtr 139 . . . . . . . . . . . 12 (b0 ∩ (a0 ∪ p0)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1)
4526lelor 166 . . . . . . . . . . . 12 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ b1) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
4644, 45letr 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 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (a0 ∪ a1) = (a1 ∪ a0)
49 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (e ∪ b1) = (b1 ∪ e)
5048, 492an 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((a1 ∪ a0) ∩ (b1 ∪ e))
51 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 ∪ a0) ∩ (b1 ∪ e)) = ((b1 ∪ e) ∩ (a1 ∪ a0))
5250, 51tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((b1 ∪ e) ∩ (a1 ∪ a0))
53 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b1 ≤ (a1 ∪ b1)
5453leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (b1 ∪ e) ≤ ((a1 ∪ b1) ∪ e)
55 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (a1 ∪ a0) ≤ ((a1 ∪ a0) ∪ e)
5654, 55le2an 169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((b1 ∪ e) ∩ (a1 ∪ a0)) ≤ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e))
5752, 56bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e))
5857df2le2 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e))) = ((a0 ∪ a1) ∩ (e ∪ b1))
5958cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 ∪ a1) ∩ (e ∪ b1)) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)))
60 anass 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ b1) ∪ e)) ∩ ((a1 ∪ a0) ∪ e)) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)))
6160cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ b1) ∪ e)) ∩ ((a1 ∪ a0) ∪ e))
6259, 61tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ b1) ∪ e)) ∩ ((a1 ∪ a0) ∪ e))
63 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (a1 ∪ a0) = (a0 ∪ a1)
6463ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a1 ∪ a0) ∪ e) = ((a0 ∪ a1) ∪ e)
65 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a0 ∪ a1) ∪ e) = ((a0 ∪ e) ∪ a1)
6664, 65tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((a1 ∪ a0) ∪ e) = ((a0 ∪ e) ∪ a1)
6766lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) = (((a1 ∪ b1) ∪ e) ∩ ((a0 ∪ e) ∪ a1))
68 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 ∪ b1) ∪ e) ∩ ((a0 ∪ e) ∪ a1)) = (((a0 ∪ e) ∪ a1) ∩ ((a1 ∪ b1) ∪ e))
6967, 68tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) = (((a0 ∪ e) ∪ a1) ∩ ((a1 ∪ b1) ∪ e))
70 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 e ≤ (a0 ∪ e)
7170ler 149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 e ≤ ((a0 ∪ e) ∪ a1)
7271mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a0 ∪ e) ∪ a1) ∩ ((a1 ∪ b1) ∪ e)) = ((((a0 ∪ e) ∪ a1) ∩ (a1 ∪ b1)) ∪ e)
73 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a0 ∪ e) ∪ a1) ∩ (a1 ∪ b1)) = ((a1 ∪ b1) ∩ ((a0 ∪ e) ∪ a1))
74 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 a1 ≤ (a1 ∪ b1)
7574mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((a1 ∪ b1) ∩ ((a0 ∪ e) ∪ a1)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ a1)
7673, 75tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a0 ∪ e) ∪ a1) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ a1)
7776ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((a0 ∪ e) ∪ a1) ∩ (a1 ∪ b1)) ∪ e) = ((((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ a1) ∪ e)
7869, 72, 773tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) = ((((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ a1) ∪ e)
79 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ a1) ∪ e) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ (a1 ∪ e))
80 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∪ (a1 ∪ e)) = ((a1 ∪ e) ∪ ((a1 ∪ b1) ∩ (a0 ∪ e)))
8178, 79, 803tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) = ((a1 ∪ e) ∪ ((a1 ∪ b1) ∩ (a0 ∪ e)))
82 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ∪ e) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
83 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ e) ∩ (a1 ∪ b1)) = ((a1 ∪ b1) ∩ (a0 ∪ e))
8483cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a1 ∪ b1) ∩ (a0 ∪ e)) = ((a0 ∪ e) ∩ (a1 ∪ b1))
85 3dp.e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 e = (b0 ∩ (a0 ∪ p0))
8685, 29tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 e = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))
8786lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (a0 ∪ e) = (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))))
8887ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ e) ∩ (a1 ∪ b1)) = ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1))
89 le1 146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b0 ≤ 1
9089leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))) ≤ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))
9190lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ≤ (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))))
9291leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) ≤ ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1))
93 an1r 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))) = (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
9493lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))
95 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))
9695cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))) = ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
97 oridm 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (a0 ∪ a0) = a0
9897ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) = (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1)))
99 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) = (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ a0)
10098, 99tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))) = (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ a0)
10194, 96, 1003tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) = (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ a0)
102101ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) = ((((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ a0) ∩ (a1 ∪ b1))
10331mlduali 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ a0) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ (a0 ∩ (a1 ∪ b1)))
104102, 103tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ (a0 ∩ (a1 ∪ b1)))
105 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a1 ∪ b1) ∩ (a1 ∪ b1)) ≤ (a1 ∪ b1)
106105leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((a1 ∪ b1) ∩ (a1 ∪ b1)) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ b1) ∪ (a0 ∩ (a1 ∪ b1)))
107104, 106bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) ≤ ((a1 ∪ b1) ∪ (a0 ∩ (a1 ∪ b1)))
108 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a1 ∪ b1) ∪ (a0 ∩ (a1 ∪ b1))) = ((a1 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b1)
109 3dp.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 d = (a1 ∪ (a0 ∩ (a1 ∪ b1)))
110109ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (d ∪ b1) = ((a1 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b1)
111110cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a1 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b1) = (d ∪ b1)
112108, 111tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a1 ∪ b1) ∪ (a0 ∩ (a1 ∪ b1))) = (d ∪ b1)
113107, 112lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b1)
11492, 113letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a1 ∪ b1))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b1)
11588, 114bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a0 ∪ e) ∩ (a1 ∪ b1)) ≤ (d ∪ b1)
11684, 115bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a1 ∪ b1) ∩ (a0 ∪ e)) ≤ (d ∪ b1)
117116df2le2 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1)) = ((a1 ∪ b1) ∩ (a0 ∪ e))
118117cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 ∪ b1) ∩ (a0 ∪ e)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1))
119 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1))
120119cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1))
121118, 120tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 ∪ b1) ∩ (a0 ∪ e)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1))
122 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a0 ∪ d) ∩ (e ∪ b1)) = ((a0 ∪ d) ∩ (e ∪ b1))
123 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 ∪ d) ∩ (b1 ∪ b1)) = ((a1 ∪ d) ∩ (b1 ∪ b1))
124 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (a0 ∪ a1) = (a1 ∪ a0)
125 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (e ∪ b1) = (b1 ∪ e)
126124, 1252an 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((a1 ∪ a0) ∩ (b1 ∪ e))
127122, 123, 126, 119dp34 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b1)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
128121, 127bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a1 ∪ b1) ∩ (a0 ∪ e)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
12982, 128lel2or 170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 ∪ e) ∪ ((a1 ∪ b1) ∩ (a0 ∪ e))) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
13081, 129bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
131130lelan 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e))) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))))
13260, 131bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ b1) ∪ e)) ∩ ((a1 ∪ a0) ∪ e)) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))))
13362, 132bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))))
134 mldual 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
135 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))
136135lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1))))
137 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ≤ ((a0 ∪ a1) ∩ (e ∪ b1))
138137ml2i 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))) = (((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))
139 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))
140 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))
141140lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
142138, 139, 1413tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
143134, 136, 1423tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
144133, 143lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
145 mldual 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))
14650ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) = (((a1 ∪ a0) ∩ (b1 ∪ e)) ∩ (a1 ∪ e))
147 anass 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a1 ∪ a0) ∩ (b1 ∪ e)) ∩ (a1 ∪ e)) = ((a1 ∪ a0) ∩ ((b1 ∪ e) ∩ (a1 ∪ e)))
148 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 e ≤ (b1 ∪ e)
149148mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((b1 ∪ e) ∩ (a1 ∪ e)) = (((b1 ∪ e) ∩ a1) ∪ e)
150 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((b1 ∪ e) ∩ a1) ∪ e) = (e ∪ ((b1 ∪ e) ∩ a1))
151 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((b1 ∪ e) ∩ a1) = (a1 ∩ (b1 ∪ e))
152151lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (e ∪ ((b1 ∪ e) ∩ a1)) = (e ∪ (a1 ∩ (b1 ∪ e)))
153149, 150, 1523tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((b1 ∪ e) ∩ (a1 ∪ e)) = (e ∪ (a1 ∩ (b1 ∪ e)))
154153lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 ∪ a0) ∩ ((b1 ∪ e) ∩ (a1 ∪ e))) = ((a1 ∪ a0) ∩ (e ∪ (a1 ∩ (b1 ∪ e))))
155 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ∩ (b1 ∪ e)) ≤ (a1 ∪ a0)
156155mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 ∪ a0) ∩ (e ∪ (a1 ∩ (b1 ∪ e)))) = (((a1 ∪ a0) ∩ e) ∪ (a1 ∩ (b1 ∪ e)))
157 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((a1 ∪ a0) ∩ e) ∪ (a1 ∩ (b1 ∪ e))) = ((a1 ∩ (b1 ∪ e)) ∪ ((a1 ∪ a0) ∩ e))
158 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 ∪ a0) ∩ e) = (e ∩ (a1 ∪ a0))
159158lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a1 ∩ (b1 ∪ e)) ∪ ((a1 ∪ a0) ∩ e)) = ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))
160157, 159tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((a1 ∪ a0) ∩ e) ∪ (a1 ∩ (b1 ∪ e))) = ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))
161154, 156, 1603tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a1 ∪ a0) ∩ ((b1 ∪ e) ∩ (a1 ∪ e))) = ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))
162146, 147, 1613tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) = ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))
163162lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
164145, 163tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
165 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ≤ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
166165leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) ≤ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
167164, 166bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) ≤ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
168144, 167letr 137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
169 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))) = ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e)))
170169lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e))))
171 or4 84 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e))))
172 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a0 ∪ d) ∩ (e ∪ b1)) = ((e ∪ b1) ∩ (a0 ∪ d))
173122, 172tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a0 ∪ d) ∩ (e ∪ b1)) = ((e ∪ b1) ∩ (a0 ∪ d))
174173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ d) ∩ (e ∪ b1)) ∪ (e ∩ (a1 ∪ a0))) = (((e ∪ b1) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0)))
175123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e)))
176174, 1752or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((e ∪ b1) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e))))
177171, 176tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((e ∪ b1) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e))))
178 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (e ∩ (a1 ∪ a0)) ≤ (e ∪ b1)
179178mli 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((e ∪ b1) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) = ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0))))
180 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a1 ∩ (b1 ∪ e)) ≤ (a1 ∪ d)
181180mli 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e))) = ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e))))
182179, 1812or 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((e ∪ b1) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (a1 ∩ (b1 ∪ e)))) = (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e)))))
183170, 177, 1823tr 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e)))))
184 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0))) = ((a0 ∪ (e ∩ (a1 ∪ a0))) ∪ d)
185 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a0 ∪ (e ∩ (a1 ∪ a0))) = (a0 ∪ (a1 ∩ (e ∪ a0)))
186 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (e ∪ a0) = (a0 ∪ e)
187186lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ∩ (e ∪ a0)) = (a1 ∩ (a0 ∪ e))
188187lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a0 ∪ (a1 ∩ (e ∪ a0))) = (a0 ∪ (a1 ∩ (a0 ∪ e)))
189185, 188tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a0 ∪ (e ∩ (a1 ∪ a0))) = (a0 ∪ (a1 ∩ (a0 ∪ e)))
190189ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 ∪ (e ∩ (a1 ∪ a0))) ∪ d) = ((a0 ∪ (a1 ∩ (a0 ∪ e))) ∪ d)
191 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0 ∪ (a1 ∩ (a0 ∪ e))) ∪ d) = ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))
192184, 190, 1913tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0))) = ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))
193192lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) = ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e))))
194 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e))) = ((b1 ∪ (a1 ∩ (b1 ∪ e))) ∪ b1)
195 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (b1 ∪ e) = (e ∪ b1)
196195lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a1 ∩ (b1 ∪ e)) = (a1 ∩ (e ∪ b1))
197196lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b1 ∪ (a1 ∩ (b1 ∪ e))) = (b1 ∪ (a1 ∩ (e ∪ b1)))
198 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b1 ∪ (a1 ∩ (e ∪ b1))) = (b1 ∪ (e ∩ (a1 ∪ b1)))
199197, 198tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (b1 ∪ (a1 ∩ (b1 ∪ e))) = (b1 ∪ (e ∩ (a1 ∪ b1)))
200199ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 ∪ (a1 ∩ (b1 ∪ e))) ∪ b1) = ((b1 ∪ (e ∩ (a1 ∪ b1))) ∪ b1)
201 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 ∪ (e ∩ (a1 ∪ b1))) ∪ b1) = ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))
202194, 200, 2013tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e))) = ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))
203202lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e)))) = ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1))))
204193, 2032or 72 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (a1 ∩ (b1 ∪ e))))) = (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))))
205183, 204tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))))
206168, 205lbtr 139 . . . . . . . . . . . . . . . . . . . . . . 23 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))))
207 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a1 ∩ (a0 ∪ e)) ≤ a1
20874leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a1 ∩ (a0 ∪ e)) ≤ ((a1 ∪ b1) ∩ (a0 ∪ e))
209208, 116letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a1 ∩ (a0 ∪ e)) ≤ (d ∪ b1)
210207, 209ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 ∩ (a0 ∪ e)) ≤ (a1 ∩ (d ∪ b1))
211210lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e))) ≤ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))
212211lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ≤ ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1))))
213 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (e ∩ (a1 ∪ b1)) ≤ e
214 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (e ∩ (a1 ∪ b1)) ≤ (a1 ∪ b1)
215 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (e ∩ (a1 ∪ b1)) ≤ (a0 ∪ e)
216214, 215ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (e ∩ (a1 ∪ b1)) ≤ ((a1 ∪ b1) ∩ (a0 ∪ e))
217216, 116letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (e ∩ (a1 ∪ b1)) ≤ (d ∪ b1)
218213, 217ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (e ∩ (a1 ∪ b1)) ≤ (e ∩ (d ∪ b1))
219218lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1))) ≤ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1)))
220219lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1)))) ≤ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1))))
221212, 220le2or 168 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (a1 ∪ b1))))) ≤ (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1)))))
222206, 221letr 137 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1)))))
223 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (d ∪ b1) = (b1 ∪ d)
224223lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a1 ∩ (d ∪ b1)) = (a1 ∩ (b1 ∪ d))
225224lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d ∪ (a1 ∩ (d ∪ b1))) = (d ∪ (a1 ∩ (b1 ∪ d)))
226 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d ∪ (a1 ∩ (b1 ∪ d))) = (d ∪ (b1 ∩ (a1 ∪ d)))
227225, 226tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ∪ (a1 ∩ (d ∪ b1))) = (d ∪ (b1 ∩ (a1 ∪ d)))
228227lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a0 ∪ (d ∪ (a1 ∩ (d ∪ b1)))) = (a0 ∪ (d ∪ (b1 ∩ (a1 ∪ d))))
229 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1))) = (a0 ∪ (d ∪ (a1 ∩ (d ∪ b1))))
230 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d))) = (a0 ∪ (d ∪ (b1 ∩ (a1 ∪ d))))
231228, 229, 2303tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1))) = ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d)))
232231lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))) = ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d))))
233 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b1 ∪ (e ∩ (d ∪ b1))) = (b1 ∪ (d ∩ (e ∪ b1)))
234233lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b1 ∪ (b1 ∪ (e ∩ (d ∪ b1)))) = (b1 ∪ (b1 ∪ (d ∩ (e ∪ b1))))
235 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1))) = (b1 ∪ (b1 ∪ (e ∩ (d ∪ b1))))
236 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1))) = (b1 ∪ (b1 ∪ (d ∩ (e ∪ b1))))
237234, 235, 2363tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1))) = ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1)))
238237lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1)))) = ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1))))
239232, 2382or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1))))) = (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1)))))
240 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b1 ∩ (a1 ∪ d)) ≤ (e ∪ b1)
241240mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d)))) = (((e ∪ b1) ∩ (a0 ∪ d)) ∪ (b1 ∩ (a1 ∪ d)))
242173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d))) = (((e ∪ b1) ∩ (a0 ∪ d)) ∪ (b1 ∩ (a1 ∪ d)))
243242cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e ∪ b1) ∩ (a0 ∪ d)) ∪ (b1 ∩ (a1 ∪ d))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d)))
244241, 243tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b1) ∩ ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d)))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d)))
245 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (d ∩ (e ∪ b1)) ≤ (a1 ∪ d)
246245mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1)))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))
247123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))
248247cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))
249246, 248tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1)))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))
250244, 2492or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (b1 ∩ (a1 ∪ d)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (d ∩ (e ∪ b1))))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1))))
251 or4 84 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))) = ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1))))
252 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) ∪ ((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1)))) = (((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1))) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))))
253 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (b1 ∩ (a1 ∪ d)) = ((a1 ∪ d) ∩ b1)
254 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b1 ≤ (b1 ∪ b1)
255254lelan 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a1 ∪ d) ∩ b1) ≤ ((a1 ∪ d) ∩ (b1 ∪ b1))
256253, 255bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b1 ∩ (a1 ∪ d)) ≤ ((a1 ∪ d) ∩ (b1 ∪ b1))
257 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 d ≤ (a0 ∪ d)
258257leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ∩ (e ∪ b1)) ≤ ((a0 ∪ d) ∩ (e ∪ b1))
259256, 258le2or 168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1))) ≤ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1)))
260123, 1222or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1)))
261260cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1))) = (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1)))
262 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
263261, 262tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ ((a0 ∪ d) ∩ (e ∪ b1))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
264259, 263lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1))) ≤ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
265264df-le2 131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((b1 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b1))) ∪ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
266251, 252, 2653tr 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((a0 ∪ d) ∩ (e ∪ b1)) ∪ (b1 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b1)) ∪ (d ∩ (e ∪ b1)))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
267239, 250, 2663tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (((e ∪ b1) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b1)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b1) ∪ (e ∩ (d ∪ b1))))) = (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
268222, 267lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1)))
26985ror 71 . . . . . . . . . . . . . . . . . . . . . 22 (e ∪ b1) = ((b0 ∩ (a0 ∪ p0)) ∪ b1)
270269lan 77 . . . . . . . . . . . . . . . . . . . . 21 ((a0 ∪ a1) ∩ (e ∪ b1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
271109lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a0 ∪ d) = (a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1))))
272271, 2692an 79 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 ∪ d) ∩ (e ∪ b1)) = ((a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
273109lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ d) = (a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1))))
274273ran 78 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 ∪ d) ∩ (b1 ∪ b1)) = ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1))
275272, 2742or 72 . . . . . . . . . . . . . . . . . . . . 21 (((a0 ∪ d) ∩ (e ∪ b1)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b1))) = (((a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1)))
276268, 270, 275le3tr2 141 . . . . . . . . . . . . . . . . . . . 20 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1)))
277 or12 80 . . . . . . . . . . . . . . . . . . . . . . 23 (a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) = (a1 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1))))
278 orabs 120 . . . . . . . . . . . . . . . . . . . . . . . 24 (a0 ∪ (a0 ∩ (a1 ∪ b1))) = a0
279278lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1)))) = (a1 ∪ a0)
280 orcom 73 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ a0) = (a0 ∪ a1)
281277, 279, 2803tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) = (a0 ∪ a1)
282281ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) = ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1))
283 orass 75 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) = (a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1))))
284283ran 78 . . . . . . . . . . . . . . . . . . . . . 22 (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1)) = ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1))
285284cm 61 . . . . . . . . . . . . . . . . . . . . 21 ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1)) = (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1))
286282, 2852or 72 . . . . . . . . . . . . . . . . . . . 20 (((a0 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ ((a1 ∪ (a1 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b1))) = (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1)))
287276, 286lbtr 139 . . . . . . . . . . . . . . . . . . 19 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1)))
288 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a1 ∪ a1) = (a1 ∪ a1)
289 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 ∪ b1) = (b1 ∪ a1)
290289lan 77 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a0 ∩ (a1 ∪ b1)) = (a0 ∩ (b1 ∪ a1))
291288, 2902or 72 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) = ((a1 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1)))
292 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1))) = (a1 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
293291, 292tr 62 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) = (a1 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
294 ml3le 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 (a1 ∪ (a0 ∩ (b1 ∪ a1))) ≤ (a1 ∪ (b1 ∩ (a0 ∪ a1)))
295294lelor 166 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1)))) ≤ (a1 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
296293, 295bltr 138 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ≤ (a1 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
297 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = (a1 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
298297cm 61 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
299288ror 71 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
300298, 299tr 62 . . . . . . . . . . . . . . . . . . . . . 22 (a1 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
301296, 300lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
302301leran 153 . . . . . . . . . . . . . . . . . . . 20 (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1)) ≤ (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1))
303302lelor 166 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b1))) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1)))
304287, 303letr 137 . . . . . . . . . . . . . . . . . 18 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1)))
30524leror 152 . . . . . . . . . . . . . . . . . . . . 21 ((b0 ∩ (a0 ∪ p0)) ∪ b1) ≤ (b0 ∪ b1)
306305lelan 167 . . . . . . . . . . . . . . . . . . . 20 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ (b0 ∪ b1))
307 leao1 162 . . . . . . . . . . . . . . . . . . . . . . 23 (b1 ∩ (a0 ∪ a1)) ≤ (b1 ∪ b1)
308307mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 ∪ b1) ∩ ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b1) ∩ (a1 ∪ a1)) ∪ (b1 ∩ (a0 ∪ a1)))
309 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 ∪ b1) ∩ ((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1))
310 ancom 74 . . . . . . . . . . . . . . . . . . . . . . 23 ((b1 ∪ b1) ∩ (a1 ∪ a1)) = ((a1 ∪ a1) ∩ (b1 ∪ b1))
311310ror 71 . . . . . . . . . . . . . . . . . . . . . 22 (((b1 ∪ b1) ∩ (a1 ∪ a1)) ∪ (b1 ∩ (a0 ∪ a1))) = (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
312308, 309, 3113tr2 64 . . . . . . . . . . . . . . . . . . . . 21 (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1)) = (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
313312bile 142 . . . . . . . . . . . . . . . . . . . 20 (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1)) ≤ (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
314306, 313le2or 168 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1))) ≤ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
315 or12 80 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
316314, 315lbtr 139 . . . . . . . . . . . . . . . . . 18 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (((a1 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b1))) ≤ (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
317304, 316letr 137 . . . . . . . . . . . . . . . . 17 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
318 3dp.c0 . . . . . . . . . . . . . . . . . . . 20 c0 = ((a1 ∪ a1) ∩ (b1 ∪ b1))
319 3dp.c1 . . . . . . . . . . . . . . . . . . . . 21 c1 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
320319ror 71 . . . . . . . . . . . . . . . . . . . 20 (c1 ∪ (b1 ∩ (a0 ∪ a1))) = (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))
321318, 3202or 72 . . . . . . . . . . . . . . . . . . 19 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1))))
322321cm 61 . . . . . . . . . . . . . . . . . 18 (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
323 orass 75 . . . . . . . . . . . . . . . . . . 19 ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
324323cm 61 . . . . . . . . . . . . . . . . . 18 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
325322, 324tr 62 . . . . . . . . . . . . . . . . 17 (((a1 ∪ a1) ∩ (b1 ∪ b1)) ∪ (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
326317, 325lbtr 139 . . . . . . . . . . . . . . . 16 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
32747, 326ler2an 173 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))))
328 lear 161 . . . . . . . . . . . . . . . 16 (b1 ∩ (a0 ∪ a1)) ≤ (a0 ∪ a1)
329328mldual2i 1127 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
330327, 329lbtr 139 . . . . . . . . . . . . . 14 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
331 lea 160 . . . . . . . . . . . . . . 15 (b1 ∩ (a0 ∪ a1)) ≤ b1
332331lelor 166 . . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1))) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
333330, 332letr 137 . . . . . . . . . . . . 13 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
334 orcom 73 . . . . . . . . . . . . 13 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1) = (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
335333, 334lbtr 139 . . . . . . . . . . . 12 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
336 leid 148 . . . . . . . . . . . 12 (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
337335, 336lel2or 170 . . . . . . . . . . 11 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
33846, 337letr 137 . . . . . . . . . 10 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
33926, 338lel2or 170 . . . . . . . . 9 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34025, 339letr 137 . . . . . . . 8 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34124, 340ler2an 173 . . . . . . 7 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
342 or32 82 . . . . . . . . . . 11 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1)
343 orcom 73 . . . . . . . . . . 11 (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1) = (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))))
344 leo 158 . . . . . . . . . . . . . . . 16 a0 ≤ (a0 ∪ a1)
345 leo 158 . . . . . . . . . . . . . . . 16 b0 ≤ (b0 ∪ b1)
346344, 345le2an 169 . . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ ((a0 ∪ a1) ∩ (b0 ∪ b1))
347 3dp.c2 . . . . . . . . . . . . . . . 16 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
348347cm 61 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = c2
349346, 348lbtr 139 . . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ c2
350319cm 61 . . . . . . . . . . . . . . . 16 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = c1
351346, 350lbtr 139 . . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ c1
352351lerr 150 . . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ (c0 ∪ c1)
353349, 352ler2an 173 . . . . . . . . . . . . 13 (a0 ∩ b0) ≤ (c2 ∩ (c0 ∪ c1))
354353df-le2 131 . . . . . . . . . . . 12 ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) = (c2 ∩ (c0 ∪ c1))
355354lor 70 . . . . . . . . . . 11 (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1)))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
356342, 343, 3553tr 65 . . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
357356lan 77 . . . . . . . . 9 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
358347ran 78 . . . . . . . . . . . . . 14 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1))
359 an32 83 . . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
360358, 359tr 62 . . . . . . . . . . . . 13 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
361360lor 70 . . . . . . . . . . . 12 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1)))
362 leor 159 . . . . . . . . . . . . 13 b1 ≤ (b0 ∪ b1)
363362ml2i 1125 . . . . . . . . . . . 12 (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))) = ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1))
364 ancom 74 . . . . . . . . . . . 12 ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1)) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
365361, 363, 3643tr 65 . . . . . . . . . . 11 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
366365lan 77 . . . . . . . . . 10 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
367 anass 76 . . . . . . . . . . 11 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
368367cm 61 . . . . . . . . . 10 (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))) = ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
369 anabs 121 . . . . . . . . . . 11 (b0 ∩ (b0 ∪ b1)) = b0
370369ran 78 . . . . . . . . . 10 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
371366, 368, 3703tr 65 . . . . . . . . 9 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
372357, 371tr 62 . . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
373372cm 61 . . . . . . 7 (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
374341, 373lbtr 139 . . . . . 6 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
375 orass 75 . . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
376 orcom 73 . . . . . . . . . 10 ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
377375, 376tr 62 . . . . . . . . 9 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
378377lan 77 . . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0)))
379 lear 161 . . . . . . . . 9 (a0 ∩ b0) ≤ b0
380379mldual2i 1127 . . . . . . . 8 (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))) = ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0))
381 orcom 73 . . . . . . . 8 ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0)) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
382378, 380, 3813tr 65 . . . . . . 7 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
383 lea 160 . . . . . . . 8 (a0 ∩ b0) ≤ a0
384383leror 152 . . . . . . 7 ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
385382, 384bltr 138 . . . . . 6 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
386374, 385letr 137 . . . . 5 (b0 ∩ (a0 ∪ p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
387386df-le2 131 . . . 4 ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))) = (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
38823, 387lbtr 139 . . 3 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3892, 388lel2or 170 . 2 (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3901, 389letr 137 1 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Colors of variables: term
Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7  1wt 8
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)
  Copyright terms: Public domain W3C validator