QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  xdp43 GIF version
Theorem xdp43 1207
Description: Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
Hypotheses
Ref Expression
xxxdp.c0 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
xxxdp.c1 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
xxxdp.c2 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
xxxdp.d d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
xxxdp.e e = (b0 ∩ (a0 ∪ p0))
xxxdp.p p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
xxxdp.p0 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
xxxdp.p2 p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))
Assertion
Ref Expression
xdp43 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Proof of Theorem xdp43
StepHypRef Expression
1 leor 159 . 2 p ≤ (a0 ∪ p)
2 leo 158 . . 3 a0 ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3 xxxdp.p . . . . . . . 8 p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))
4 anass 76 . . . . . . . 8 (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2)) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
53, 4tr 62 . . . . . . 7 p = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
6 xxxdp.p0 . . . . . . . . . . 11 p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))
76lan 77 . . . . . . . . . 10 ((a0 ∪ b0) ∩ p0) = ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
87cm 61 . . . . . . . . 9 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = ((a0 ∪ b0) ∩ p0)
9 leao4 165 . . . . . . . . 9 ((a0 ∪ b0) ∩ p0) ≤ (a0 ∪ p0)
108, 9bltr 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)
1311, 12lbtr 139 . . . . . . . 8 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (b0 ∪ a0)
1410, 13ler2an 173 . . . . . . 7 ((a0 ∪ b0) ∩ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ ((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) ∩ (a2 ∪ b2)))
2928lan 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)
3231lelor 166 . . . . . . . . . . . . . . . . 17 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) ≤ (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) ∩ (a2 ∪ b2))) ≤ ((a0 ∪ a1) ∪ b1)
3630, 35letr 137 . . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ ((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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
83 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ e) ∩ (a1 ∪ b1)) = ((a1 ∪ b1) ∩ (a0 ∪ e))
8483cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a1 ∪ b1) ∩ (a0 ∪ e)) = ((a0 ∪ e) ∩ (a1 ∪ b1))
85 xxxdp.e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 e = (b0 ∩ (a0 ∪ p0))
8685, 29tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 e = (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
8786lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (a0 ∪ e) = (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))))
8887ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ e) ∩ (a1 ∪ b1)) = ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1))
89 le1 146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 b0 ≤ 1
9089leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) ≤ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
9190lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ≤ (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))))
9291leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1))
93 an1r 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
9493lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
95 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))
9695cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (a0 ∪ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))) = ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
97 oridm 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (a0 ∪ a0) = a0
9897ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2)))
99 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
10098, 99tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((a0 ∪ a0) ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
10194, 96, 1003tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0)
102101ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) = ((((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0) ∩ (a1 ∪ b1))
10331mlduali 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ a0) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1)))
104102, 103tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) = (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1)))
105 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((a1 ∪ b1) ∩ (a2 ∪ b2)) ≤ (a2 ∪ b2)
106105leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((a1 ∪ b1) ∩ (a2 ∪ b2)) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1)))
107104, 106bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1)))
108 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1))) = ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2)
109 xxxdp.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))
110109ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (d ∪ b2) = ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2)
111110cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((a2 ∪ (a0 ∩ (a1 ∪ b1))) ∪ b2) = (d ∪ b2)
112108, 111tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((a2 ∪ b2) ∪ (a0 ∩ (a1 ∪ b1))) = (d ∪ b2)
113107, 112lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((a0 ∪ (1 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
11492, 113letr 137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1 ∪ b1) ∩ (a2 ∪ b2))))) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
11588, 114bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((a0 ∪ e) ∩ (a1 ∪ b1)) ≤ (d ∪ b2)
11684, 115bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((a1 ∪ b1) ∩ (a0 ∪ e)) ≤ (d ∪ b2)
117116df2le2 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2)) = ((a1 ∪ b1) ∩ (a0 ∪ e))
118117cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 ∪ b1) ∩ (a0 ∪ e)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2))
119 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2))
120119cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2))
121118, 120tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((a1 ∪ b1) ∩ (a0 ∪ e)) = (((a1 ∪ b1) ∩ (a0 ∪ e)) ∩ (d ∪ b2))
122 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a0 ∪ d) ∩ (e ∪ b2)) = ((a0 ∪ d) ∩ (e ∪ b2))
123 id 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((a1 ∪ d) ∩ (b1 ∪ b2)) = ((a1 ∪ d) ∩ (b1 ∪ b2))
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 ∪ b2)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
128121, 127bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((a1 ∪ b1) ∩ (a0 ∪ e)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
12982, 128lel2or 170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a1 ∪ e) ∪ ((a1 ∪ b1) ∩ (a0 ∪ e))) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
13081, 129bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((a1 ∪ b1) ∪ e) ∩ ((a1 ∪ a0) ∪ e)) ≤ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))))
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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))))
13362, 132bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))))
134 mldual 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
135 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))
136135lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∩ ((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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))) = (((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))
139 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))
140 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))
141140lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
142138, 139, 1413tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)) ∪ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∩ ((a0 ∪ a1) ∩ (e ∪ b1)))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
143134, 136, 1423tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((a1 ∪ e) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))))) = (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
144133, 143lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))))
145 mldual 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∪ (((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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
164145, 163tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) = ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
165 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
166165leror 152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) ≤ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
167164, 166bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ (((a0 ∪ a1) ∩ (e ∪ b1)) ∩ (a1 ∪ e)))) ≤ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0))))
168144, 167letr 137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((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 ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e))))
171 or4 84 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e))))
172 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((a0 ∪ d) ∩ (e ∪ b2)) = ((e ∪ b2) ∩ (a0 ∪ d))
173122, 172tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a0 ∪ d) ∩ (e ∪ b2)) = ((e ∪ b2) ∩ (a0 ∪ d))
174173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a0 ∪ d) ∩ (e ∪ b2)) ∪ (e ∩ (a1 ∪ a0))) = (((e ∪ b2) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0)))
175123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e)))
176174, 1752or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((e ∪ b2) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e))))
177171, 176tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((e ∩ (a1 ∪ a0)) ∪ (a1 ∩ (b1 ∪ e)))) = ((((e ∪ b2) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e))))
178 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (e ∩ (a1 ∪ a0)) ≤ (e ∪ b2)
179178mli 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((e ∪ b2) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) = ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0))))
180 leao1 162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a1 ∩ (b1 ∪ e)) ≤ (a1 ∪ d)
181180mli 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e))) = ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e))))
182179, 1812or 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((e ∪ b2) ∩ (a0 ∪ d)) ∪ (e ∩ (a1 ∪ a0))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (a1 ∩ (b1 ∪ e)))) = (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e)))))
183170, 177, 1823tr 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (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 ∪ b2) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) = ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e))))
194 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e))) = ((b1 ∪ (a1 ∩ (b1 ∪ e))) ∪ b2)
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))) ∪ b2) = ((b1 ∪ (e ∩ (a1 ∪ b1))) ∪ b2)
201 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((b1 ∪ (e ∩ (a1 ∪ b1))) ∪ b2) = ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1)))
202194, 200, 2013tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e))) = ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1)))
203202lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e)))) = ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1))))
204193, 2032or 72 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (e ∩ (a1 ∪ a0)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (a1 ∩ (b1 ∪ e))))) = (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1)))))
205183, 204tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((a1 ∩ (b1 ∪ e)) ∪ (e ∩ (a1 ∪ a0)))) = (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1)))))
206168, 205lbtr 139 . . . . . . . . . . . . . . . . . . . . . . 23 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (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 ∪ b2)
210207, 209ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 ∩ (a0 ∪ e)) ≤ (a1 ∩ (d ∪ b2))
211210lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e))) ≤ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))
212211lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ≤ ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2))))
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 ∪ b2)
218213, 217ler2an 173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (e ∩ (a1 ∪ b1)) ≤ (e ∩ (d ∪ b2))
219218lelor 166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1))) ≤ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2)))
220219lelan 167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1)))) ≤ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2))))
221212, 220le2or 168 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (a0 ∪ e)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (a1 ∪ b1))))) ≤ (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2)))))
222206, 221letr 137 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2)))))
223 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (d ∪ b2) = (b2 ∪ d)
224223lan 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a1 ∩ (d ∪ b2)) = (a1 ∩ (b2 ∪ d))
225224lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d ∪ (a1 ∩ (d ∪ b2))) = (d ∪ (a1 ∩ (b2 ∪ d)))
226 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (d ∪ (a1 ∩ (b2 ∪ d))) = (d ∪ (b2 ∩ (a1 ∪ d)))
227225, 226tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ∪ (a1 ∩ (d ∪ b2))) = (d ∪ (b2 ∩ (a1 ∪ d)))
228227lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a0 ∪ (d ∪ (a1 ∩ (d ∪ b2)))) = (a0 ∪ (d ∪ (b2 ∩ (a1 ∪ d))))
229 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2))) = (a0 ∪ (d ∪ (a1 ∩ (d ∪ b2))))
230 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d))) = (a0 ∪ (d ∪ (b2 ∩ (a1 ∪ d))))
231228, 229, 2303tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2))) = ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d)))
232231lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))) = ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d))))
233 ml3 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b2 ∪ (e ∩ (d ∪ b2))) = (b2 ∪ (d ∩ (e ∪ b2)))
234233lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b1 ∪ (b2 ∪ (e ∩ (d ∪ b2)))) = (b1 ∪ (b2 ∪ (d ∩ (e ∪ b2))))
235 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2))) = (b1 ∪ (b2 ∪ (e ∩ (d ∪ b2))))
236 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2))) = (b1 ∪ (b2 ∪ (d ∩ (e ∪ b2))))
237234, 235, 2363tr1 63 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2))) = ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2)))
238237lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2)))) = ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2))))
239232, 2382or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2))))) = (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2)))))
240 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b2 ∩ (a1 ∪ d)) ≤ (e ∪ b2)
241240mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d)))) = (((e ∪ b2) ∩ (a0 ∪ d)) ∪ (b2 ∩ (a1 ∪ d)))
242173ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d))) = (((e ∪ b2) ∩ (a0 ∪ d)) ∪ (b2 ∩ (a1 ∪ d)))
243242cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((e ∪ b2) ∩ (a0 ∪ d)) ∪ (b2 ∩ (a1 ∪ d))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d)))
244241, 243tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((e ∪ b2) ∩ ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d)))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d)))
245 leao3 164 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (d ∩ (e ∪ b2)) ≤ (a1 ∪ d)
246245mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2)))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))
247123ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))
248247cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))
249246, 248tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2)))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))
250244, 2492or 72 . . . . . . . . . . . . . . . . . . . . . . 23 (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (b2 ∩ (a1 ∪ d)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (d ∩ (e ∪ b2))))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2))))
251 or4 84 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))) = ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2))))
252 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) ∪ ((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2)))) = (((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2))) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))))
253 ancom 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (b2 ∩ (a1 ∪ d)) = ((a1 ∪ d) ∩ b2)
254 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b2 ≤ (b1 ∪ b2)
255254lelan 167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a1 ∪ d) ∩ b2) ≤ ((a1 ∪ d) ∩ (b1 ∪ b2))
256253, 255bltr 138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b2 ∩ (a1 ∪ d)) ≤ ((a1 ∪ d) ∩ (b1 ∪ b2))
257 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 d ≤ (a0 ∪ d)
258257leran 153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (d ∩ (e ∪ b2)) ≤ ((a0 ∪ d) ∩ (e ∪ b2))
259256, 258le2or 168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2))) ≤ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2)))
260123, 1222or 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2)))
261260cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2))) = (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2)))
262 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
263261, 262tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ ((a0 ∪ d) ∩ (e ∪ b2))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
264259, 263lbtr 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2))) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
265264df-le2 131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((b2 ∩ (a1 ∪ d)) ∪ (d ∩ (e ∪ b2))) ∪ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
266251, 252, 2653tr 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((a0 ∪ d) ∩ (e ∪ b2)) ∪ (b2 ∩ (a1 ∪ d))) ∪ (((a1 ∪ d) ∩ (b1 ∪ b2)) ∪ (d ∩ (e ∪ b2)))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
267239, 250, 2663tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (((e ∪ b2) ∩ ((a0 ∪ d) ∪ (a1 ∩ (d ∪ b2)))) ∪ ((a1 ∪ d) ∩ ((b1 ∪ b2) ∪ (e ∩ (d ∪ b2))))) = (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
268222, 267lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a0 ∪ a1) ∩ (e ∪ b1)) ≤ (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2)))
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 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
27285ror 71 . . . . . . . . . . . . . . . . . . . . . . 23 (e ∪ b2) = ((b0 ∩ (a0 ∪ p0)) ∪ b2)
273271, 2722an 79 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 ∪ d) ∩ (e ∪ b2)) = ((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2))
274109lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a1 ∪ d) = (a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
275274ran 78 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 ∪ d) ∩ (b1 ∪ b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))
276273, 2752or 72 . . . . . . . . . . . . . . . . . . . . 21 (((a0 ∪ d) ∩ (e ∪ b2)) ∪ ((a1 ∪ d) ∩ (b1 ∪ b2))) = (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
277268, 270, 276le3tr2 141 . . . . . . . . . . . . . . . . . . . 20 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)))
278 or12 80 . . . . . . . . . . . . . . . . . . . . . . 23 (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) = (a2 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1))))
279 orabs 120 . . . . . . . . . . . . . . . . . . . . . . . 24 (a0 ∪ (a0 ∩ (a1 ∪ b1))) = a0
280279lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 ∪ (a0 ∪ (a0 ∩ (a1 ∪ b1)))) = (a2 ∪ a0)
281 orcom 73 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 ∪ a0) = (a0 ∪ a2)
282278, 280, 2813tr 65 . . . . . . . . . . . . . . . . . . . . . 22 (a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) = (a0 ∪ a2)
283282ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) = ((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2))
284 orass 75 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = (a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1))))
285284ran 78 . . . . . . . . . . . . . . . . . . . . . 22 (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))
286285cm 61 . . . . . . . . . . . . . . . . . . . . 21 ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2)) = (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))
287283, 2862or 72 . . . . . . . . . . . . . . . . . . . 20 (((a0 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1 ∪ b1)))) ∩ (b1 ∪ b2))) = (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)))
288277, 287lbtr 139 . . . . . . . . . . . . . . . . . . 19 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)))
289 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a1 ∪ a2) = (a2 ∪ a1)
290 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a1 ∪ b1) = (b1 ∪ a1)
291290lan 77 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a0 ∩ (a1 ∪ b1)) = (a0 ∩ (b1 ∪ a1))
292289, 2912or 72 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1)))
293 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a2 ∪ a1) ∪ (a0 ∩ (b1 ∪ a1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
294292, 293tr 62 . . . . . . . . . . . . . . . . . . . . . . 23 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1))))
295 ml3le 1129 . . . . . . . . . . . . . . . . . . . . . . . 24 (a1 ∪ (a0 ∩ (b1 ∪ a1))) ≤ (a1 ∪ (b1 ∩ (a0 ∪ a1)))
296295lelor 166 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 ∪ (a1 ∪ (a0 ∩ (b1 ∪ a1)))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
297294, 296bltr 138 . . . . . . . . . . . . . . . . . . . . . 22 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
298 orass 75 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1))))
299298cm 61 . . . . . . . . . . . . . . . . . . . . . . 23 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1)))
300 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (a2 ∪ a1) = (a1 ∪ a2)
301300ror 71 . . . . . . . . . . . . . . . . . . . . . . 23 ((a2 ∪ a1) ∪ (b1 ∩ (a0 ∪ a1))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
302299, 301tr 62 . . . . . . . . . . . . . . . . . . . . . 22 (a2 ∪ (a1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
303297, 302lbtr 139 . . . . . . . . . . . . . . . . . . . . 21 ((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ≤ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))
304303leran 153 . . . . . . . . . . . . . . . . . . . 20 (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2)) ≤ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))
305304lelor 166 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (a0 ∩ (a1 ∪ b1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))
306288, 305letr 137 . . . . . . . . . . . . . . . . . 18 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)))
30724leror 152 . . . . . . . . . . . . . . . . . . . . 21 ((b0 ∩ (a0 ∪ p0)) ∪ b2) ≤ (b0 ∪ b2)
308307lelan 167 . . . . . . . . . . . . . . . . . . . 20 ((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
309 leao1 162 . . . . . . . . . . . . . . . . . . . . . . 23 (b1 ∩ (a0 ∪ a1)) ≤ (b1 ∪ b2)
310309mldual2i 1127 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) = (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1)))
311 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 ((b1 ∪ b2) ∩ ((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))
312 ancom 74 . . . . . . . . . . . . . . . . . . . . . . 23 ((b1 ∪ b2) ∩ (a1 ∪ a2)) = ((a1 ∪ a2) ∩ (b1 ∪ b2))
313312ror 71 . . . . . . . . . . . . . . . . . . . . . 22 (((b1 ∪ b2) ∩ (a1 ∪ a2)) ∪ (b1 ∩ (a0 ∪ a1))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
314310, 311, 3133tr2 64 . . . . . . . . . . . . . . . . . . . . 21 (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
315314bile 142 . . . . . . . . . . . . . . . . . . . 20 (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2)) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
316308, 315le2or 168 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
317 or12 80 . . . . . . . . . . . . . . . . . . 19 (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
318316, 317lbtr 139 . . . . . . . . . . . . . . . . . 18 (((a0 ∪ a2) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b2)) ∪ (((a1 ∪ a2) ∪ (b1 ∩ (a0 ∪ a1))) ∩ (b1 ∪ b2))) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
319306, 318letr 137 . . . . . . . . . . . . . . . . 17 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
320 xxxdp.c0 . . . . . . . . . . . . . . . . . . . 20 c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))
321 xxxdp.c1 . . . . . . . . . . . . . . . . . . . . 21 c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))
322321ror 71 . . . . . . . . . . . . . . . . . . . 20 (c1 ∪ (b1 ∩ (a0 ∪ a1))) = (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))
323320, 3222or 72 . . . . . . . . . . . . . . . . . . 19 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1))))
324323cm 61 . . . . . . . . . . . . . . . . . 18 (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
325 orass 75 . . . . . . . . . . . . . . . . . . 19 ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1))))
326325cm 61 . . . . . . . . . . . . . . . . . 18 (c0 ∪ (c1 ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
327324, 326tr 62 . . . . . . . . . . . . . . . . 17 (((a1 ∪ a2) ∩ (b1 ∪ b2)) ∪ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ (b1 ∩ (a0 ∪ a1)))) = ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
328319, 327lbtr 139 . . . . . . . . . . . . . . . 16 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
32947, 328ler2an 173 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1))))
330 lear 161 . . . . . . . . . . . . . . . 16 (b1 ∩ (a0 ∪ a1)) ≤ (a0 ∪ a1)
331330mldual2i 1127 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
332329, 331lbtr 139 . . . . . . . . . . . . . 14 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1)))
333 lea 160 . . . . . . . . . . . . . . 15 (b1 ∩ (a0 ∪ a1)) ≤ b1
334333lelor 166 . . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ (b1 ∩ (a0 ∪ a1))) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
335332, 334letr 137 . . . . . . . . . . . . 13 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1)
336 orcom 73 . . . . . . . . . . . . 13 (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∪ b1) = (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
337335, 336lbtr 139 . . . . . . . . . . . 12 ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
338 leid 148 . . . . . . . . . . . 12 (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
339337, 338lel2or 170 . . . . . . . . . . 11 (((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ∪ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34046, 339letr 137 . . . . . . . . . 10 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34126, 340lel2or 170 . . . . . . . . 9 (b1 ∪ (b0 ∩ (a0 ∪ p0))) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34225, 341letr 137 . . . . . . . 8 (b0 ∩ (a0 ∪ p0)) ≤ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))
34324, 342ler2an 173 . . . . . . 7 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
344 or32 82 . . . . . . . . . . 11 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1)
345 orcom 73 . . . . . . . . . . 11 (((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) ∪ b1) = (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))))
346 leo 158 . . . . . . . . . . . . . . . 16 a0 ≤ (a0 ∪ a1)
347 leo 158 . . . . . . . . . . . . . . . 16 b0 ≤ (b0 ∪ b1)
348346, 347le2an 169 . . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ ((a0 ∪ a1) ∩ (b0 ∪ b1))
349 xxxdp.c2 . . . . . . . . . . . . . . . 16 c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))
350349cm 61 . . . . . . . . . . . . . . 15 ((a0 ∪ a1) ∩ (b0 ∪ b1)) = c2
351348, 350lbtr 139 . . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ c2
352 leo 158 . . . . . . . . . . . . . . . . 17 a0 ≤ (a0 ∪ a2)
353 leo 158 . . . . . . . . . . . . . . . . 17 b0 ≤ (b0 ∪ b2)
354352, 353le2an 169 . . . . . . . . . . . . . . . 16 (a0 ∩ b0) ≤ ((a0 ∪ a2) ∩ (b0 ∪ b2))
355321cm 61 . . . . . . . . . . . . . . . 16 ((a0 ∪ a2) ∩ (b0 ∪ b2)) = c1
356354, 355lbtr 139 . . . . . . . . . . . . . . 15 (a0 ∩ b0) ≤ c1
357356lerr 150 . . . . . . . . . . . . . 14 (a0 ∩ b0) ≤ (c0 ∪ c1)
358351, 357ler2an 173 . . . . . . . . . . . . 13 (a0 ∩ b0) ≤ (c2 ∩ (c0 ∪ c1))
359358df-le2 131 . . . . . . . . . . . 12 ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1))) = (c2 ∩ (c0 ∪ c1))
360359lor 70 . . . . . . . . . . 11 (b1 ∪ ((a0 ∩ b0) ∪ (c2 ∩ (c0 ∪ c1)))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
361344, 345, 3603tr 65 . . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (c2 ∩ (c0 ∪ c1)))
362361lan 77 . . . . . . . . 9 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
363349ran 78 . . . . . . . . . . . . . 14 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1))
364 an32 83 . . . . . . . . . . . . . 14 (((a0 ∪ a1) ∩ (b0 ∪ b1)) ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
365363, 364tr 62 . . . . . . . . . . . . 13 (c2 ∩ (c0 ∪ c1)) = (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))
366365lor 70 . . . . . . . . . . . 12 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1)))
367 leor 159 . . . . . . . . . . . . 13 b1 ≤ (b0 ∪ b1)
368367ml2i 1125 . . . . . . . . . . . 12 (b1 ∪ (((a0 ∪ a1) ∩ (c0 ∪ c1)) ∩ (b0 ∪ b1))) = ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1))
369 ancom 74 . . . . . . . . . . . 12 ((b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))) ∩ (b0 ∪ b1)) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
370366, 368, 3693tr 65 . . . . . . . . . . 11 (b1 ∪ (c2 ∩ (c0 ∪ c1))) = ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
371370lan 77 . . . . . . . . . 10 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
372 anass 76 . . . . . . . . . . 11 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))))
373372cm 61 . . . . . . . . . 10 (b0 ∩ ((b0 ∪ b1) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))) = ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
374 anabs 121 . . . . . . . . . . 11 (b0 ∩ (b0 ∪ b1)) = b0
375374ran 78 . . . . . . . . . 10 ((b0 ∩ (b0 ∪ b1)) ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
376371, 373, 3753tr 65 . . . . . . . . 9 (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
377362, 376tr 62 . . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1))))
378377cm 61 . . . . . . 7 (b0 ∩ (b1 ∪ ((a0 ∪ a1) ∩ (c0 ∪ c1)))) = (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
379343, 378lbtr 139 . . . . . 6 (b0 ∩ (a0 ∪ p0)) ≤ (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))))
380 orass 75 . . . . . . . . . 10 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
381 orcom 73 . . . . . . . . . 10 ((a0 ∩ b0) ∪ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
382380, 381tr 62 . . . . . . . . 9 (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1))) = ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))
383382lan 77 . . . . . . . 8 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0)))
384 lear 161 . . . . . . . . 9 (a0 ∩ b0) ≤ b0
385384mldual2i 1127 . . . . . . . 8 (b0 ∩ ((b1 ∪ (c2 ∩ (c0 ∪ c1))) ∪ (a0 ∩ b0))) = ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0))
386 orcom 73 . . . . . . . 8 ((b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))) ∪ (a0 ∩ b0)) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
387383, 385, 3863tr 65 . . . . . . 7 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
388 lea 160 . . . . . . . 8 (a0 ∩ b0) ≤ a0
389388leror 152 . . . . . . 7 ((a0 ∩ b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
390387, 389bltr 138 . . . . . 6 (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
391379, 390letr 137 . . . . 5 (b0 ∩ (a0 ∪ p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
392391df-le2 131 . . . 4 ((b0 ∩ (a0 ∪ p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))) = (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
39323, 392lbtr 139 . . 3 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3942, 393lel2or 170 . 2 (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
3951, 394letr 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