QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  xdp45 GIF version

Theorem xdp45 1206
Description: Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
Hypotheses
Ref Expression
xxxdp.c0 c0 = ((a1a2) ∩ (b1b2))
xxxdp.c1 c1 = ((a0a2) ∩ (b0b2))
xxxdp.c2 c2 = ((a0a1) ∩ (b0b1))
xxxdp.d d = (a2 ∪ (a0 ∩ (a1b1)))
xxxdp.e e = (b0 ∩ (a0p0))
xxxdp.p p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
xxxdp.p0 p0 = ((a1b1) ∩ (a2b2))
xxxdp.p2 p2 = ((a0b0) ∩ (a1b1))
Assertion
Ref Expression
xdp45 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Proof of Theorem xdp45
StepHypRef Expression
1 ax-a2 31 . . . . . . . . . . . . . . . . . 18 (a0a1) = (a1a0)
2 ax-a2 31 . . . . . . . . . . . . . . . . . 18 (eb1) = (b1e)
31, 22an 79 . . . . . . . . . . . . . . . . 17 ((a0a1) ∩ (eb1)) = ((a1a0) ∩ (b1e))
4 ancom 74 . . . . . . . . . . . . . . . . 17 ((a1a0) ∩ (b1e)) = ((b1e) ∩ (a1a0))
53, 4tr 62 . . . . . . . . . . . . . . . 16 ((a0a1) ∩ (eb1)) = ((b1e) ∩ (a1a0))
6 leor 159 . . . . . . . . . . . . . . . . . 18 b1 ≤ (a1b1)
76leror 152 . . . . . . . . . . . . . . . . 17 (b1e) ≤ ((a1b1) ∪ e)
8 leo 158 . . . . . . . . . . . . . . . . 17 (a1a0) ≤ ((a1a0) ∪ e)
97, 8le2an 169 . . . . . . . . . . . . . . . 16 ((b1e) ∩ (a1a0)) ≤ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e))
105, 9bltr 138 . . . . . . . . . . . . . . 15 ((a0a1) ∩ (eb1)) ≤ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e))
1110df2le2 136 . . . . . . . . . . . . . 14 (((a0a1) ∩ (eb1)) ∩ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e))) = ((a0a1) ∩ (eb1))
1211cm 61 . . . . . . . . . . . . 13 ((a0a1) ∩ (eb1)) = (((a0a1) ∩ (eb1)) ∩ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)))
13 anass 76 . . . . . . . . . . . . . 14 ((((a0a1) ∩ (eb1)) ∩ ((a1b1) ∪ e)) ∩ ((a1a0) ∪ e)) = (((a0a1) ∩ (eb1)) ∩ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)))
1413cm 61 . . . . . . . . . . . . 13 (((a0a1) ∩ (eb1)) ∩ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e))) = ((((a0a1) ∩ (eb1)) ∩ ((a1b1) ∪ e)) ∩ ((a1a0) ∪ e))
1512, 14tr 62 . . . . . . . . . . . 12 ((a0a1) ∩ (eb1)) = ((((a0a1) ∩ (eb1)) ∩ ((a1b1) ∪ e)) ∩ ((a1a0) ∪ e))
16 ax-a2 31 . . . . . . . . . . . . . . . . . . . . 21 (a1a0) = (a0a1)
1716ror 71 . . . . . . . . . . . . . . . . . . . 20 ((a1a0) ∪ e) = ((a0a1) ∪ e)
18 or32 82 . . . . . . . . . . . . . . . . . . . 20 ((a0a1) ∪ e) = ((a0e) ∪ a1)
1917, 18tr 62 . . . . . . . . . . . . . . . . . . 19 ((a1a0) ∪ e) = ((a0e) ∪ a1)
2019lan 77 . . . . . . . . . . . . . . . . . 18 (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)) = (((a1b1) ∪ e) ∩ ((a0e) ∪ a1))
21 ancom 74 . . . . . . . . . . . . . . . . . 18 (((a1b1) ∪ e) ∩ ((a0e) ∪ a1)) = (((a0e) ∪ a1) ∩ ((a1b1) ∪ e))
2220, 21tr 62 . . . . . . . . . . . . . . . . 17 (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)) = (((a0e) ∪ a1) ∩ ((a1b1) ∪ e))
23 leor 159 . . . . . . . . . . . . . . . . . . 19 e ≤ (a0e)
2423ler 149 . . . . . . . . . . . . . . . . . 18 e ≤ ((a0e) ∪ a1)
2524mldual2i 1127 . . . . . . . . . . . . . . . . 17 (((a0e) ∪ a1) ∩ ((a1b1) ∪ e)) = ((((a0e) ∪ a1) ∩ (a1b1)) ∪ e)
26 ancom 74 . . . . . . . . . . . . . . . . . . 19 (((a0e) ∪ a1) ∩ (a1b1)) = ((a1b1) ∩ ((a0e) ∪ a1))
27 leo 158 . . . . . . . . . . . . . . . . . . . 20 a1 ≤ (a1b1)
2827mldual2i 1127 . . . . . . . . . . . . . . . . . . 19 ((a1b1) ∩ ((a0e) ∪ a1)) = (((a1b1) ∩ (a0e)) ∪ a1)
2926, 28tr 62 . . . . . . . . . . . . . . . . . 18 (((a0e) ∪ a1) ∩ (a1b1)) = (((a1b1) ∩ (a0e)) ∪ a1)
3029ror 71 . . . . . . . . . . . . . . . . 17 ((((a0e) ∪ a1) ∩ (a1b1)) ∪ e) = ((((a1b1) ∩ (a0e)) ∪ a1) ∪ e)
3122, 25, 303tr 65 . . . . . . . . . . . . . . . 16 (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)) = ((((a1b1) ∩ (a0e)) ∪ a1) ∪ e)
32 orass 75 . . . . . . . . . . . . . . . 16 ((((a1b1) ∩ (a0e)) ∪ a1) ∪ e) = (((a1b1) ∩ (a0e)) ∪ (a1e))
33 orcom 73 . . . . . . . . . . . . . . . 16 (((a1b1) ∩ (a0e)) ∪ (a1e)) = ((a1e) ∪ ((a1b1) ∩ (a0e)))
3431, 32, 333tr 65 . . . . . . . . . . . . . . 15 (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)) = ((a1e) ∪ ((a1b1) ∩ (a0e)))
35 leo 158 . . . . . . . . . . . . . . . 16 (a1e) ≤ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
36 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 ((a0e) ∩ (a1b1)) = ((a1b1) ∩ (a0e))
3736cm 61 . . . . . . . . . . . . . . . . . . . . 21 ((a1b1) ∩ (a0e)) = ((a0e) ∩ (a1b1))
38 xxxdp.e . . . . . . . . . . . . . . . . . . . . . . . . 25 e = (b0 ∩ (a0p0))
39 xxxdp.p0 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 p0 = ((a1b1) ∩ (a2b2))
4039lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a0p0) = (a0 ∪ ((a1b1) ∩ (a2b2)))
4140lan 77 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b0 ∩ (a0p0)) = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
4238, 41tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 e = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
4342lor 70 . . . . . . . . . . . . . . . . . . . . . . 23 (a0e) = (a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))))
4443ran 78 . . . . . . . . . . . . . . . . . . . . . 22 ((a0e) ∩ (a1b1)) = ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1))
45 le1 146 . . . . . . . . . . . . . . . . . . . . . . . . . 26 b0 ≤ 1
4645leran 153 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
4746lelor 166 . . . . . . . . . . . . . . . . . . . . . . . 24 (a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ≤ (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))))
4847leran 153 . . . . . . . . . . . . . . . . . . . . . . 23 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1))
49 an1r 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) = (a0 ∪ ((a1b1) ∩ (a2b2)))
5049lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) = (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2))))
51 orass 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2))))
5251cm 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2)))) = ((a0a0) ∪ ((a1b1) ∩ (a2b2)))
53 oridm 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a0a0) = a0
5453ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (a0 ∪ ((a1b1) ∩ (a2b2)))
55 orcom 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a0 ∪ ((a1b1) ∩ (a2b2))) = (((a1b1) ∩ (a2b2)) ∪ a0)
5654, 55tr 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (((a1b1) ∩ (a2b2)) ∪ a0)
5750, 52, 563tr 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) = (((a1b1) ∩ (a2b2)) ∪ a0)
5857ran 78 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) = ((((a1b1) ∩ (a2b2)) ∪ a0) ∩ (a1b1))
59 lea 160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a1b1) ∩ (a2b2)) ≤ (a1b1)
6059mlduali 1128 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a1b1) ∩ (a2b2)) ∪ a0) ∩ (a1b1)) = (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1)))
6158, 60tr 62 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) = (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1)))
62 lear 161 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a1b1) ∩ (a2b2)) ≤ (a2b2)
6362leror 152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1))) ≤ ((a2b2) ∪ (a0 ∩ (a1b1)))
6461, 63bltr 138 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ ((a2b2) ∪ (a0 ∩ (a1b1)))
65 or32 82 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a2b2) ∪ (a0 ∩ (a1b1))) = ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2)
66 xxxdp.d . . . . . . . . . . . . . . . . . . . . . . . . . . 27 d = (a2 ∪ (a0 ∩ (a1b1)))
6766ror 71 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (db2) = ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2)
6867cm 61 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2) = (db2)
6965, 68tr 62 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a2b2) ∪ (a0 ∩ (a1b1))) = (db2)
7064, 69lbtr 139 . . . . . . . . . . . . . . . . . . . . . . 23 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ (db2)
7148, 70letr 137 . . . . . . . . . . . . . . . . . . . . . 22 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ (db2)
7244, 71bltr 138 . . . . . . . . . . . . . . . . . . . . 21 ((a0e) ∩ (a1b1)) ≤ (db2)
7337, 72bltr 138 . . . . . . . . . . . . . . . . . . . 20 ((a1b1) ∩ (a0e)) ≤ (db2)
7473df2le2 136 . . . . . . . . . . . . . . . . . . 19 (((a1b1) ∩ (a0e)) ∩ (db2)) = ((a1b1) ∩ (a0e))
7574cm 61 . . . . . . . . . . . . . . . . . 18 ((a1b1) ∩ (a0e)) = (((a1b1) ∩ (a0e)) ∩ (db2))
76 id 59 . . . . . . . . . . . . . . . . . . 19 (((a1b1) ∩ (a0e)) ∩ (db2)) = (((a1b1) ∩ (a0e)) ∩ (db2))
7776cm 61 . . . . . . . . . . . . . . . . . 18 (((a1b1) ∩ (a0e)) ∩ (db2)) = (((a1b1) ∩ (a0e)) ∩ (db2))
7875, 77tr 62 . . . . . . . . . . . . . . . . 17 ((a1b1) ∩ (a0e)) = (((a1b1) ∩ (a0e)) ∩ (db2))
79 id 59 . . . . . . . . . . . . . . . . . 18 ((a0d) ∩ (eb2)) = ((a0d) ∩ (eb2))
80 id 59 . . . . . . . . . . . . . . . . . 18 ((a1d) ∩ (b1b2)) = ((a1d) ∩ (b1b2))
81 orcom 73 . . . . . . . . . . . . . . . . . . 19 (a0a1) = (a1a0)
82 orcom 73 . . . . . . . . . . . . . . . . . . 19 (eb1) = (b1e)
8381, 822an 79 . . . . . . . . . . . . . . . . . 18 ((a0a1) ∩ (eb1)) = ((a1a0) ∩ (b1e))
8479, 80, 83, 76dp34 1181 . . . . . . . . . . . . . . . . 17 (((a1b1) ∩ (a0e)) ∩ (db2)) ≤ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
8578, 84bltr 138 . . . . . . . . . . . . . . . 16 ((a1b1) ∩ (a0e)) ≤ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
8635, 85lel2or 170 . . . . . . . . . . . . . . 15 ((a1e) ∪ ((a1b1) ∩ (a0e))) ≤ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
8734, 86bltr 138 . . . . . . . . . . . . . 14 (((a1b1) ∪ e) ∩ ((a1a0) ∪ e)) ≤ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
8887lelan 167 . . . . . . . . . . . . 13 (((a0a1) ∩ (eb1)) ∩ (((a1b1) ∪ e) ∩ ((a1a0) ∪ e))) ≤ (((a0a1) ∩ (eb1)) ∩ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))))
8913, 88bltr 138 . . . . . . . . . . . 12 ((((a0a1) ∩ (eb1)) ∩ ((a1b1) ∪ e)) ∩ ((a1a0) ∪ e)) ≤ (((a0a1) ∩ (eb1)) ∩ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))))
9015, 89bltr 138 . . . . . . . . . . 11 ((a0a1) ∩ (eb1)) ≤ (((a0a1) ∩ (eb1)) ∩ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))))
91 mldual 1124 . . . . . . . . . . . 12 (((a0a1) ∩ (eb1)) ∩ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))) = ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
92 ancom 74 . . . . . . . . . . . . 13 (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) = ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∩ ((a0a1) ∩ (eb1)))
9392lor 70 . . . . . . . . . . . 12 ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))) = ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∩ ((a0a1) ∩ (eb1))))
94 lea 160 . . . . . . . . . . . . . 14 (((a0a1) ∩ (eb1)) ∩ (a1e)) ≤ ((a0a1) ∩ (eb1))
9594ml2i 1125 . . . . . . . . . . . . 13 ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∩ ((a0a1) ∩ (eb1)))) = (((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∩ ((a0a1) ∩ (eb1)))
96 ancom 74 . . . . . . . . . . . . 13 (((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∩ ((a0a1) ∩ (eb1))) = (((a0a1) ∩ (eb1)) ∩ ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))
97 ax-a2 31 . . . . . . . . . . . . . 14 ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) = ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e)))
9897lan 77 . . . . . . . . . . . . 13 (((a0a1) ∩ (eb1)) ∩ ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))) = (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e))))
9995, 96, 983tr 65 . . . . . . . . . . . 12 ((((a0a1) ∩ (eb1)) ∩ (a1e)) ∪ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∩ ((a0a1) ∩ (eb1)))) = (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e))))
10091, 93, 993tr 65 . . . . . . . . . . 11 (((a0a1) ∩ (eb1)) ∩ ((a1e) ∪ (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))))) = (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e))))
10190, 100lbtr 139 . . . . . . . . . 10 ((a0a1) ∩ (eb1)) ≤ (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e))))
102 mldual 1124 . . . . . . . . . . . 12 (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e)))) = ((((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e)))
1033ran 78 . . . . . . . . . . . . . 14 (((a0a1) ∩ (eb1)) ∩ (a1e)) = (((a1a0) ∩ (b1e)) ∩ (a1e))
104 anass 76 . . . . . . . . . . . . . 14 (((a1a0) ∩ (b1e)) ∩ (a1e)) = ((a1a0) ∩ ((b1e) ∩ (a1e)))
105 leor 159 . . . . . . . . . . . . . . . . . 18 e ≤ (b1e)
106105mldual2i 1127 . . . . . . . . . . . . . . . . 17 ((b1e) ∩ (a1e)) = (((b1e) ∩ a1) ∪ e)
107 orcom 73 . . . . . . . . . . . . . . . . 17 (((b1e) ∩ a1) ∪ e) = (e ∪ ((b1e) ∩ a1))
108 ancom 74 . . . . . . . . . . . . . . . . . 18 ((b1e) ∩ a1) = (a1 ∩ (b1e))
109108lor 70 . . . . . . . . . . . . . . . . 17 (e ∪ ((b1e) ∩ a1)) = (e ∪ (a1 ∩ (b1e)))
110106, 107, 1093tr 65 . . . . . . . . . . . . . . . 16 ((b1e) ∩ (a1e)) = (e ∪ (a1 ∩ (b1e)))
111110lan 77 . . . . . . . . . . . . . . 15 ((a1a0) ∩ ((b1e) ∩ (a1e))) = ((a1a0) ∩ (e ∪ (a1 ∩ (b1e))))
112 leao1 162 . . . . . . . . . . . . . . . 16 (a1 ∩ (b1e)) ≤ (a1a0)
113112mldual2i 1127 . . . . . . . . . . . . . . 15 ((a1a0) ∩ (e ∪ (a1 ∩ (b1e)))) = (((a1a0) ∩ e) ∪ (a1 ∩ (b1e)))
114 orcom 73 . . . . . . . . . . . . . . . 16 (((a1a0) ∩ e) ∪ (a1 ∩ (b1e))) = ((a1 ∩ (b1e)) ∪ ((a1a0) ∩ e))
115 ancom 74 . . . . . . . . . . . . . . . . 17 ((a1a0) ∩ e) = (e ∩ (a1a0))
116115lor 70 . . . . . . . . . . . . . . . 16 ((a1 ∩ (b1e)) ∪ ((a1a0) ∩ e)) = ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))
117114, 116tr 62 . . . . . . . . . . . . . . 15 (((a1a0) ∩ e) ∪ (a1 ∩ (b1e))) = ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))
118111, 113, 1173tr 65 . . . . . . . . . . . . . 14 ((a1a0) ∩ ((b1e) ∩ (a1e))) = ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))
119103, 104, 1183tr 65 . . . . . . . . . . . . 13 (((a0a1) ∩ (eb1)) ∩ (a1e)) = ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))
120119lor 70 . . . . . . . . . . . 12 ((((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e))) = ((((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))))
121102, 120tr 62 . . . . . . . . . . 11 (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e)))) = ((((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))))
122 lear 161 . . . . . . . . . . . 12 (((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
123122leror 152 . . . . . . . . . . 11 ((((a0a1) ∩ (eb1)) ∩ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))) ≤ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))))
124121, 123bltr 138 . . . . . . . . . 10 (((a0a1) ∩ (eb1)) ∩ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ (((a0a1) ∩ (eb1)) ∩ (a1e)))) ≤ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))))
125101, 124letr 137 . . . . . . . . 9 ((a0a1) ∩ (eb1)) ≤ ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))))
126 orcom 73 . . . . . . . . . . . 12 ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0))) = ((e ∩ (a1a0)) ∪ (a1 ∩ (b1e)))
127126lor 70 . . . . . . . . . . 11 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))) = ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((e ∩ (a1a0)) ∪ (a1 ∩ (b1e))))
128 or4 84 . . . . . . . . . . . 12 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((e ∩ (a1a0)) ∪ (a1 ∩ (b1e)))) = ((((a0d) ∩ (eb2)) ∪ (e ∩ (a1a0))) ∪ (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e))))
129 ancom 74 . . . . . . . . . . . . . . 15 ((a0d) ∩ (eb2)) = ((eb2) ∩ (a0d))
13079, 129tr 62 . . . . . . . . . . . . . 14 ((a0d) ∩ (eb2)) = ((eb2) ∩ (a0d))
131130ror 71 . . . . . . . . . . . . 13 (((a0d) ∩ (eb2)) ∪ (e ∩ (a1a0))) = (((eb2) ∩ (a0d)) ∪ (e ∩ (a1a0)))
13280ror 71 . . . . . . . . . . . . 13 (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e))) = (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e)))
133131, 1322or 72 . . . . . . . . . . . 12 ((((a0d) ∩ (eb2)) ∪ (e ∩ (a1a0))) ∪ (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e)))) = ((((eb2) ∩ (a0d)) ∪ (e ∩ (a1a0))) ∪ (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e))))
134128, 133tr 62 . . . . . . . . . . 11 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((e ∩ (a1a0)) ∪ (a1 ∩ (b1e)))) = ((((eb2) ∩ (a0d)) ∪ (e ∩ (a1a0))) ∪ (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e))))
135 leao1 162 . . . . . . . . . . . . 13 (e ∩ (a1a0)) ≤ (eb2)
136135mli 1126 . . . . . . . . . . . 12 (((eb2) ∩ (a0d)) ∪ (e ∩ (a1a0))) = ((eb2) ∩ ((a0d) ∪ (e ∩ (a1a0))))
137 leao1 162 . . . . . . . . . . . . 13 (a1 ∩ (b1e)) ≤ (a1d)
138137mli 1126 . . . . . . . . . . . 12 (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e))) = ((a1d) ∩ ((b1b2) ∪ (a1 ∩ (b1e))))
139136, 1382or 72 . . . . . . . . . . 11 ((((eb2) ∩ (a0d)) ∪ (e ∩ (a1a0))) ∪ (((a1d) ∩ (b1b2)) ∪ (a1 ∩ (b1e)))) = (((eb2) ∩ ((a0d) ∪ (e ∩ (a1a0)))) ∪ ((a1d) ∩ ((b1b2) ∪ (a1 ∩ (b1e)))))
140127, 134, 1393tr 65 . . . . . . . . . 10 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))) = (((eb2) ∩ ((a0d) ∪ (e ∩ (a1a0)))) ∪ ((a1d) ∩ ((b1b2) ∪ (a1 ∩ (b1e)))))
141 or32 82 . . . . . . . . . . . . 13 ((a0d) ∪ (e ∩ (a1a0))) = ((a0 ∪ (e ∩ (a1a0))) ∪ d)
142 ml3 1130 . . . . . . . . . . . . . . 15 (a0 ∪ (e ∩ (a1a0))) = (a0 ∪ (a1 ∩ (ea0)))
143 orcom 73 . . . . . . . . . . . . . . . . 17 (ea0) = (a0e)
144143lan 77 . . . . . . . . . . . . . . . 16 (a1 ∩ (ea0)) = (a1 ∩ (a0e))
145144lor 70 . . . . . . . . . . . . . . 15 (a0 ∪ (a1 ∩ (ea0))) = (a0 ∪ (a1 ∩ (a0e)))
146142, 145tr 62 . . . . . . . . . . . . . 14 (a0 ∪ (e ∩ (a1a0))) = (a0 ∪ (a1 ∩ (a0e)))
147146ror 71 . . . . . . . . . . . . 13 ((a0 ∪ (e ∩ (a1a0))) ∪ d) = ((a0 ∪ (a1 ∩ (a0e))) ∪ d)
148 or32 82 . . . . . . . . . . . . 13 ((a0 ∪ (a1 ∩ (a0e))) ∪ d) = ((a0d) ∪ (a1 ∩ (a0e)))
149141, 147, 1483tr 65 . . . . . . . . . . . 12 ((a0d) ∪ (e ∩ (a1a0))) = ((a0d) ∪ (a1 ∩ (a0e)))
150149lan 77 . . . . . . . . . . 11 ((eb2) ∩ ((a0d) ∪ (e ∩ (a1a0)))) = ((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e))))
151 or32 82 . . . . . . . . . . . . 13 ((b1b2) ∪ (a1 ∩ (b1e))) = ((b1 ∪ (a1 ∩ (b1e))) ∪ b2)
152 orcom 73 . . . . . . . . . . . . . . . . 17 (b1e) = (eb1)
153152lan 77 . . . . . . . . . . . . . . . 16 (a1 ∩ (b1e)) = (a1 ∩ (eb1))
154153lor 70 . . . . . . . . . . . . . . 15 (b1 ∪ (a1 ∩ (b1e))) = (b1 ∪ (a1 ∩ (eb1)))
155 ml3 1130 . . . . . . . . . . . . . . 15 (b1 ∪ (a1 ∩ (eb1))) = (b1 ∪ (e ∩ (a1b1)))
156154, 155tr 62 . . . . . . . . . . . . . 14 (b1 ∪ (a1 ∩ (b1e))) = (b1 ∪ (e ∩ (a1b1)))
157156ror 71 . . . . . . . . . . . . 13 ((b1 ∪ (a1 ∩ (b1e))) ∪ b2) = ((b1 ∪ (e ∩ (a1b1))) ∪ b2)
158 or32 82 . . . . . . . . . . . . 13 ((b1 ∪ (e ∩ (a1b1))) ∪ b2) = ((b1b2) ∪ (e ∩ (a1b1)))
159151, 157, 1583tr 65 . . . . . . . . . . . 12 ((b1b2) ∪ (a1 ∩ (b1e))) = ((b1b2) ∪ (e ∩ (a1b1)))
160159lan 77 . . . . . . . . . . 11 ((a1d) ∩ ((b1b2) ∪ (a1 ∩ (b1e)))) = ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1))))
161150, 1602or 72 . . . . . . . . . 10 (((eb2) ∩ ((a0d) ∪ (e ∩ (a1a0)))) ∪ ((a1d) ∩ ((b1b2) ∪ (a1 ∩ (b1e))))) = (((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1)))))
162140, 161tr 62 . . . . . . . . 9 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((a1 ∩ (b1e)) ∪ (e ∩ (a1a0)))) = (((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1)))))
163125, 162lbtr 139 . . . . . . . 8 ((a0a1) ∩ (eb1)) ≤ (((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1)))))
164 lea 160 . . . . . . . . . . . 12 (a1 ∩ (a0e)) ≤ a1
16527leran 153 . . . . . . . . . . . . 13 (a1 ∩ (a0e)) ≤ ((a1b1) ∩ (a0e))
166165, 73letr 137 . . . . . . . . . . . 12 (a1 ∩ (a0e)) ≤ (db2)
167164, 166ler2an 173 . . . . . . . . . . 11 (a1 ∩ (a0e)) ≤ (a1 ∩ (db2))
168167lelor 166 . . . . . . . . . 10 ((a0d) ∪ (a1 ∩ (a0e))) ≤ ((a0d) ∪ (a1 ∩ (db2)))
169168lelan 167 . . . . . . . . 9 ((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e)))) ≤ ((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2))))
170 lea 160 . . . . . . . . . . . 12 (e ∩ (a1b1)) ≤ e
171 lear 161 . . . . . . . . . . . . . 14 (e ∩ (a1b1)) ≤ (a1b1)
172 leao3 164 . . . . . . . . . . . . . 14 (e ∩ (a1b1)) ≤ (a0e)
173171, 172ler2an 173 . . . . . . . . . . . . 13 (e ∩ (a1b1)) ≤ ((a1b1) ∩ (a0e))
174173, 73letr 137 . . . . . . . . . . . 12 (e ∩ (a1b1)) ≤ (db2)
175170, 174ler2an 173 . . . . . . . . . . 11 (e ∩ (a1b1)) ≤ (e ∩ (db2))
176175lelor 166 . . . . . . . . . 10 ((b1b2) ∪ (e ∩ (a1b1))) ≤ ((b1b2) ∪ (e ∩ (db2)))
177176lelan 167 . . . . . . . . 9 ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1)))) ≤ ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2))))
178169, 177le2or 168 . . . . . . . 8 (((eb2) ∩ ((a0d) ∪ (a1 ∩ (a0e)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (a1b1))))) ≤ (((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2)))))
179163, 178letr 137 . . . . . . 7 ((a0a1) ∩ (eb1)) ≤ (((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2)))))
180 ax-a2 31 . . . . . . . . . . . . . . 15 (db2) = (b2d)
181180lan 77 . . . . . . . . . . . . . 14 (a1 ∩ (db2)) = (a1 ∩ (b2d))
182181lor 70 . . . . . . . . . . . . 13 (d ∪ (a1 ∩ (db2))) = (d ∪ (a1 ∩ (b2d)))
183 ml3 1130 . . . . . . . . . . . . 13 (d ∪ (a1 ∩ (b2d))) = (d ∪ (b2 ∩ (a1d)))
184182, 183tr 62 . . . . . . . . . . . 12 (d ∪ (a1 ∩ (db2))) = (d ∪ (b2 ∩ (a1d)))
185184lor 70 . . . . . . . . . . 11 (a0 ∪ (d ∪ (a1 ∩ (db2)))) = (a0 ∪ (d ∪ (b2 ∩ (a1d))))
186 orass 75 . . . . . . . . . . 11 ((a0d) ∪ (a1 ∩ (db2))) = (a0 ∪ (d ∪ (a1 ∩ (db2))))
187 orass 75 . . . . . . . . . . 11 ((a0d) ∪ (b2 ∩ (a1d))) = (a0 ∪ (d ∪ (b2 ∩ (a1d))))
188185, 186, 1873tr1 63 . . . . . . . . . 10 ((a0d) ∪ (a1 ∩ (db2))) = ((a0d) ∪ (b2 ∩ (a1d)))
189188lan 77 . . . . . . . . 9 ((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2)))) = ((eb2) ∩ ((a0d) ∪ (b2 ∩ (a1d))))
190 ml3 1130 . . . . . . . . . . . 12 (b2 ∪ (e ∩ (db2))) = (b2 ∪ (d ∩ (eb2)))
191190lor 70 . . . . . . . . . . 11 (b1 ∪ (b2 ∪ (e ∩ (db2)))) = (b1 ∪ (b2 ∪ (d ∩ (eb2))))
192 orass 75 . . . . . . . . . . 11 ((b1b2) ∪ (e ∩ (db2))) = (b1 ∪ (b2 ∪ (e ∩ (db2))))
193 orass 75 . . . . . . . . . . 11 ((b1b2) ∪ (d ∩ (eb2))) = (b1 ∪ (b2 ∪ (d ∩ (eb2))))
194191, 192, 1933tr1 63 . . . . . . . . . 10 ((b1b2) ∪ (e ∩ (db2))) = ((b1b2) ∪ (d ∩ (eb2)))
195194lan 77 . . . . . . . . 9 ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2)))) = ((a1d) ∩ ((b1b2) ∪ (d ∩ (eb2))))
196189, 1952or 72 . . . . . . . 8 (((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2))))) = (((eb2) ∩ ((a0d) ∪ (b2 ∩ (a1d)))) ∪ ((a1d) ∩ ((b1b2) ∪ (d ∩ (eb2)))))
197 leao3 164 . . . . . . . . . . 11 (b2 ∩ (a1d)) ≤ (eb2)
198197mldual2i 1127 . . . . . . . . . 10 ((eb2) ∩ ((a0d) ∪ (b2 ∩ (a1d)))) = (((eb2) ∩ (a0d)) ∪ (b2 ∩ (a1d)))
199130ror 71 . . . . . . . . . . 11 (((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d))) = (((eb2) ∩ (a0d)) ∪ (b2 ∩ (a1d)))
200199cm 61 . . . . . . . . . 10 (((eb2) ∩ (a0d)) ∪ (b2 ∩ (a1d))) = (((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d)))
201198, 200tr 62 . . . . . . . . 9 ((eb2) ∩ ((a0d) ∪ (b2 ∩ (a1d)))) = (((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d)))
202 leao3 164 . . . . . . . . . . 11 (d ∩ (eb2)) ≤ (a1d)
203202mldual2i 1127 . . . . . . . . . 10 ((a1d) ∩ ((b1b2) ∪ (d ∩ (eb2)))) = (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))
20480ror 71 . . . . . . . . . . 11 (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2))) = (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))
205204cm 61 . . . . . . . . . 10 (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2))) = (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))
206203, 205tr 62 . . . . . . . . 9 ((a1d) ∩ ((b1b2) ∪ (d ∩ (eb2)))) = (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))
207201, 2062or 72 . . . . . . . 8 (((eb2) ∩ ((a0d) ∪ (b2 ∩ (a1d)))) ∪ ((a1d) ∩ ((b1b2) ∪ (d ∩ (eb2))))) = ((((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d))) ∪ (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2))))
208 or4 84 . . . . . . . . 9 ((((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d))) ∪ (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))) = ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((b2 ∩ (a1d)) ∪ (d ∩ (eb2))))
209 orcom 73 . . . . . . . . 9 ((((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) ∪ ((b2 ∩ (a1d)) ∪ (d ∩ (eb2)))) = (((b2 ∩ (a1d)) ∪ (d ∩ (eb2))) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))))
210 ancom 74 . . . . . . . . . . . . 13 (b2 ∩ (a1d)) = ((a1d) ∩ b2)
211 leor 159 . . . . . . . . . . . . . 14 b2 ≤ (b1b2)
212211lelan 167 . . . . . . . . . . . . 13 ((a1d) ∩ b2) ≤ ((a1d) ∩ (b1b2))
213210, 212bltr 138 . . . . . . . . . . . 12 (b2 ∩ (a1d)) ≤ ((a1d) ∩ (b1b2))
214 leor 159 . . . . . . . . . . . . 13 d ≤ (a0d)
215214leran 153 . . . . . . . . . . . 12 (d ∩ (eb2)) ≤ ((a0d) ∩ (eb2))
216213, 215le2or 168 . . . . . . . . . . 11 ((b2 ∩ (a1d)) ∪ (d ∩ (eb2))) ≤ (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2)))
21780, 792or 72 . . . . . . . . . . . . 13 (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2))) = (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2)))
218217cm 61 . . . . . . . . . . . 12 (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2))) = (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2)))
219 orcom 73 . . . . . . . . . . . 12 (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2))) = (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
220218, 219tr 62 . . . . . . . . . . 11 (((a1d) ∩ (b1b2)) ∪ ((a0d) ∩ (eb2))) = (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
221216, 220lbtr 139 . . . . . . . . . 10 ((b2 ∩ (a1d)) ∪ (d ∩ (eb2))) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
222221df-le2 131 . . . . . . . . 9 (((b2 ∩ (a1d)) ∪ (d ∩ (eb2))) ∪ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))) = (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
223208, 209, 2223tr 65 . . . . . . . 8 ((((a0d) ∩ (eb2)) ∪ (b2 ∩ (a1d))) ∪ (((a1d) ∩ (b1b2)) ∪ (d ∩ (eb2)))) = (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
224196, 207, 2233tr 65 . . . . . . 7 (((eb2) ∩ ((a0d) ∪ (a1 ∩ (db2)))) ∪ ((a1d) ∩ ((b1b2) ∪ (e ∩ (db2))))) = (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
225179, 224lbtr 139 . . . . . 6 ((a0a1) ∩ (eb1)) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
22638ror 71 . . . . . . 7 (eb1) = ((b0 ∩ (a0p0)) ∪ b1)
227226lan 77 . . . . . 6 ((a0a1) ∩ (eb1)) = ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1))
22866lor 70 . . . . . . . 8 (a0d) = (a0 ∪ (a2 ∪ (a0 ∩ (a1b1))))
22938ror 71 . . . . . . . 8 (eb2) = ((b0 ∩ (a0p0)) ∪ b2)
230228, 2292an 79 . . . . . . 7 ((a0d) ∩ (eb2)) = ((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2))
23166lor 70 . . . . . . . 8 (a1d) = (a1 ∪ (a2 ∪ (a0 ∩ (a1b1))))
232231ran 78 . . . . . . 7 ((a1d) ∩ (b1b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))
233230, 2322or 72 . . . . . 6 (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) = (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)))
234225, 227, 233le3tr2 141 . . . . 5 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)))
235 or12 80 . . . . . . . 8 (a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) = (a2 ∪ (a0 ∪ (a0 ∩ (a1b1))))
236 orabs 120 . . . . . . . . 9 (a0 ∪ (a0 ∩ (a1b1))) = a0
237236lor 70 . . . . . . . 8 (a2 ∪ (a0 ∪ (a0 ∩ (a1b1)))) = (a2a0)
238 orcom 73 . . . . . . . 8 (a2a0) = (a0a2)
239235, 237, 2383tr 65 . . . . . . 7 (a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) = (a0a2)
240239ran 78 . . . . . 6 ((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) = ((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2))
241 orass 75 . . . . . . . 8 ((a1a2) ∪ (a0 ∩ (a1b1))) = (a1 ∪ (a2 ∪ (a0 ∩ (a1b1))))
242241ran 78 . . . . . . 7 (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))
243242cm 61 . . . . . 6 ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)) = (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2))
244240, 2432or 72 . . . . 5 (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))) = (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)))
245234, 244lbtr 139 . . . 4 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)))
246 ax-a2 31 . . . . . . . . . 10 (a1a2) = (a2a1)
247 ax-a2 31 . . . . . . . . . . 11 (a1b1) = (b1a1)
248247lan 77 . . . . . . . . . 10 (a0 ∩ (a1b1)) = (a0 ∩ (b1a1))
249246, 2482or 72 . . . . . . . . 9 ((a1a2) ∪ (a0 ∩ (a1b1))) = ((a2a1) ∪ (a0 ∩ (b1a1)))
250 orass 75 . . . . . . . . 9 ((a2a1) ∪ (a0 ∩ (b1a1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1a1))))
251249, 250tr 62 . . . . . . . 8 ((a1a2) ∪ (a0 ∩ (a1b1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1a1))))
252 ml3le 1129 . . . . . . . . 9 (a1 ∪ (a0 ∩ (b1a1))) ≤ (a1 ∪ (b1 ∩ (a0a1)))
253252lelor 166 . . . . . . . 8 (a2 ∪ (a1 ∪ (a0 ∩ (b1a1)))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
254251, 253bltr 138 . . . . . . 7 ((a1a2) ∪ (a0 ∩ (a1b1))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
255 orass 75 . . . . . . . . 9 ((a2a1) ∪ (b1 ∩ (a0a1))) = (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
256255cm 61 . . . . . . . 8 (a2 ∪ (a1 ∪ (b1 ∩ (a0a1)))) = ((a2a1) ∪ (b1 ∩ (a0a1)))
257 ax-a2 31 . . . . . . . . 9 (a2a1) = (a1a2)
258257ror 71 . . . . . . . 8 ((a2a1) ∪ (b1 ∩ (a0a1))) = ((a1a2) ∪ (b1 ∩ (a0a1)))
259256, 258tr 62 . . . . . . 7 (a2 ∪ (a1 ∪ (b1 ∩ (a0a1)))) = ((a1a2) ∪ (b1 ∩ (a0a1)))
260254, 259lbtr 139 . . . . . 6 ((a1a2) ∪ (a0 ∩ (a1b1))) ≤ ((a1a2) ∪ (b1 ∩ (a0a1)))
261260leran 153 . . . . 5 (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)) ≤ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))
262261lelor 166 . . . 4 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2))) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)))
263245, 262letr 137 . . 3 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)))
264 lea 160 . . . . . . 7 (b0 ∩ (a0p0)) ≤ b0
265264leror 152 . . . . . 6 ((b0 ∩ (a0p0)) ∪ b2) ≤ (b0b2)
266265lelan 167 . . . . 5 ((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ≤ ((a0a2) ∩ (b0b2))
267 leao1 162 . . . . . . . 8 (b1 ∩ (a0a1)) ≤ (b1b2)
268267mldual2i 1127 . . . . . . 7 ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) = (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1)))
269 ancom 74 . . . . . . 7 ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))
270 ancom 74 . . . . . . . 8 ((b1b2) ∩ (a1a2)) = ((a1a2) ∩ (b1b2))
271270ror 71 . . . . . . 7 (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) = (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
272268, 269, 2713tr2 64 . . . . . 6 (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)) = (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
273272bile 142 . . . . 5 (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)) ≤ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
274266, 273le2or 168 . . . 4 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))) ≤ (((a0a2) ∩ (b0b2)) ∪ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1))))
275 or12 80 . . . 4 (((a0a2) ∩ (b0b2)) ∪ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
276274, 275lbtr 139 . . 3 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))) ≤ (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
277263, 276letr 137 . 2 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
278 xxxdp.c0 . . . . 5 c0 = ((a1a2) ∩ (b1b2))
279 xxxdp.c1 . . . . . 6 c1 = ((a0a2) ∩ (b0b2))
280279ror 71 . . . . 5 (c1 ∪ (b1 ∩ (a0a1))) = (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))
281278, 2802or 72 . . . 4 (c0 ∪ (c1 ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
282281cm 61 . . 3 (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0a1))))
283 orass 75 . . . 4 ((c0c1) ∪ (b1 ∩ (a0a1))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0a1))))
284283cm 61 . . 3 (c0 ∪ (c1 ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ (b1 ∩ (a0a1)))
285282, 284tr 62 . 2 (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ (b1 ∩ (a0a1)))
286277, 285lbtr 139 1 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))
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