xdp45lem - Quantum Logic Explorer

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

Theorem xdp45lem 1204

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

**Hypotheses**
Ref	Expression
xxdp.1	p₂ ≤ (a₂ ∪ b₂)
xxdp.c0	c₀ = ((a₁ ∪ a₂) ∩ (b₁ ∪ b₂))
xxdp.c1	c₁ = ((a₀ ∪ a₂) ∩ (b₀ ∪ b₂))
xxdp.c2	c₂ = ((a₀ ∪ a₁) ∩ (b₀ ∪ b₁))
xxdp.d	d = (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))
xxdp.e	e = (b₀ ∩ (a₀ ∪ p₀))
xxdp.p	p = (((a₀ ∪ b₀) ∩ (a₁ ∪ b₁)) ∩ (a₂ ∪ b₂))
xxdp.p0	p₀ = ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))
xxdp.p2	p₂ = ((a₀ ∪ b₀) ∩ (a₁ ∪ b₁))

**Assertion**
Ref	Expression
xdp45lem	((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ ((c₀ ∪ c₁) ∪ (b₁ ∩ (a₀ ∪ a₁)))

**Proof of Theorem xdp45lem**
Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . . . . . . . . . . . . 18 (a₀ ∪ a₁) = (a₁ ∪ a₀)
2		ax-a2 31	. . . . . . . . . . . . . . . . . 18 (e ∪ b₁) = (b₁ ∪ e)
3	1, 2	2an 79	. . . . . . . . . . . . . . . . 17 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = ((a₁ ∪ a₀) ∩ (b₁ ∪ e))
4		ancom 74	. . . . . . . . . . . . . . . . 17 ((a₁ ∪ a₀) ∩ (b₁ ∪ e)) = ((b₁ ∪ e) ∩ (a₁ ∪ a₀))
5	3, 4	tr 62	. . . . . . . . . . . . . . . 16 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = ((b₁ ∪ e) ∩ (a₁ ∪ a₀))
6		leor 159	. . . . . . . . . . . . . . . . . 18 b₁ ≤ (a₁ ∪ b₁)
7	6	leror 152	. . . . . . . . . . . . . . . . 17 (b₁ ∪ e) ≤ ((a₁ ∪ b₁) ∪ e)
8		leo 158	. . . . . . . . . . . . . . . . 17 (a₁ ∪ a₀) ≤ ((a₁ ∪ a₀) ∪ e)
9	7, 8	le2an 169	. . . . . . . . . . . . . . . 16 ((b₁ ∪ e) ∩ (a₁ ∪ a₀)) ≤ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e))
10	5, 9	bltr 138	. . . . . . . . . . . . . . 15 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e))
11	10	df2le2 136	. . . . . . . . . . . . . 14 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e))) = ((a₀ ∪ a₁) ∩ (e ∪ b₁))
12	11	cm 61	. . . . . . . . . . . . 13 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)))
13		anass 76	. . . . . . . . . . . . . 14 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ b₁) ∪ e)) ∩ ((a₁ ∪ a₀) ∪ e)) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)))
14	13	cm 61	. . . . . . . . . . . . 13 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ b₁) ∪ e)) ∩ ((a₁ ∪ a₀) ∪ e))
15	12, 14	tr 62	. . . . . . . . . . . 12 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ b₁) ∪ e)) ∩ ((a₁ ∪ a₀) ∪ e))
16		ax-a2 31	. . . . . . . . . . . . . . . . . . . . 21 (a₁ ∪ a₀) = (a₀ ∪ a₁)
17	16	ror 71	. . . . . . . . . . . . . . . . . . . 20 ((a₁ ∪ a₀) ∪ e) = ((a₀ ∪ a₁) ∪ e)
18		or32 82	. . . . . . . . . . . . . . . . . . . 20 ((a₀ ∪ a₁) ∪ e) = ((a₀ ∪ e) ∪ a₁)
19	17, 18	tr 62	. . . . . . . . . . . . . . . . . . 19 ((a₁ ∪ a₀) ∪ e) = ((a₀ ∪ e) ∪ a₁)
20	19	lan 77	. . . . . . . . . . . . . . . . . 18 (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)) = (((a₁ ∪ b₁) ∪ e) ∩ ((a₀ ∪ e) ∪ a₁))
21		ancom 74	. . . . . . . . . . . . . . . . . 18 (((a₁ ∪ b₁) ∪ e) ∩ ((a₀ ∪ e) ∪ a₁)) = (((a₀ ∪ e) ∪ a₁) ∩ ((a₁ ∪ b₁) ∪ e))
22	20, 21	tr 62	. . . . . . . . . . . . . . . . 17 (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)) = (((a₀ ∪ e) ∪ a₁) ∩ ((a₁ ∪ b₁) ∪ e))
23		leor 159	. . . . . . . . . . . . . . . . . . 19 e ≤ (a₀ ∪ e)
24	23	ler 149	. . . . . . . . . . . . . . . . . 18 e ≤ ((a₀ ∪ e) ∪ a₁)
25	24	mldual2i 1127	. . . . . . . . . . . . . . . . 17 (((a₀ ∪ e) ∪ a₁) ∩ ((a₁ ∪ b₁) ∪ e)) = ((((a₀ ∪ e) ∪ a₁) ∩ (a₁ ∪ b₁)) ∪ e)
26		ancom 74	. . . . . . . . . . . . . . . . . . 19 (((a₀ ∪ e) ∪ a₁) ∩ (a₁ ∪ b₁)) = ((a₁ ∪ b₁) ∩ ((a₀ ∪ e) ∪ a₁))
27		leo 158	. . . . . . . . . . . . . . . . . . . 20 a₁ ≤ (a₁ ∪ b₁)
28	27	mldual2i 1127	. . . . . . . . . . . . . . . . . . 19 ((a₁ ∪ b₁) ∩ ((a₀ ∪ e) ∪ a₁)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ a₁)
29	26, 28	tr 62	. . . . . . . . . . . . . . . . . 18 (((a₀ ∪ e) ∪ a₁) ∩ (a₁ ∪ b₁)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ a₁)
30	29	ror 71	. . . . . . . . . . . . . . . . 17 ((((a₀ ∪ e) ∪ a₁) ∩ (a₁ ∪ b₁)) ∪ e) = ((((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ a₁) ∪ e)
31	22, 25, 30	3tr 65	. . . . . . . . . . . . . . . 16 (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)) = ((((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ a₁) ∪ e)
32		orass 75	. . . . . . . . . . . . . . . 16 ((((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ a₁) ∪ e) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ (a₁ ∪ e))
33		orcom 73	. . . . . . . . . . . . . . . 16 (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∪ (a₁ ∪ e)) = ((a₁ ∪ e) ∪ ((a₁ ∪ b₁) ∩ (a₀ ∪ e)))
34	31, 32, 33	3tr 65	. . . . . . . . . . . . . . 15 (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)) = ((a₁ ∪ e) ∪ ((a₁ ∪ b₁) ∩ (a₀ ∪ e)))
35		leo 158	. . . . . . . . . . . . . . . 16 (a₁ ∪ e) ≤ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
36		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 ((a₀ ∪ e) ∩ (a₁ ∪ b₁)) = ((a₁ ∪ b₁) ∩ (a₀ ∪ e))
37	36	cm 61	. . . . . . . . . . . . . . . . . . . . 21 ((a₁ ∪ b₁) ∩ (a₀ ∪ e)) = ((a₀ ∪ e) ∩ (a₁ ∪ b₁))
38		xxdp.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 e = (b₀ ∩ (a₀ ∪ p₀))
39		xxdp.p0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 p₀ = ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))
40	39	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (a₀ ∪ p₀) = (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))
41	40	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . 25 (b₀ ∩ (a₀ ∪ p₀)) = (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))
42	38, 41	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 e = (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))
43	42	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 (a₀ ∪ e) = (a₀ ∪ (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))))
44	43	ran 78	. . . . . . . . . . . . . . . . . . . . . 22 ((a₀ ∪ e) ∩ (a₁ ∪ b₁)) = ((a₀ ∪ (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁))
45		le1 146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b₀ ≤ 1
46	45	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . 25 (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))) ≤ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))
47	46	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . 24 (a₀ ∪ (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ≤ (a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))))
48	47	leran 153	. . . . . . . . . . . . . . . . . . . . . . 23 ((a₀ ∪ (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) ≤ ((a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁))
49		an1r 107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))) = (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))
50	49	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) = (a₀ ∪ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))
51		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a₀ ∪ a₀) ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))) = (a₀ ∪ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))
52	51	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (a₀ ∪ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))) = ((a₀ ∪ a₀) ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))
53		oridm 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (a₀ ∪ a₀) = a₀
54	53	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((a₀ ∪ a₀) ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))) = (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)))
55		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))) = (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ a₀)
56	54, 55	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((a₀ ∪ a₀) ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))) = (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ a₀)
57	50, 52, 56	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) = (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ a₀)
58	57	ran 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) = ((((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ a₀) ∩ (a₁ ∪ b₁))
59		lea 160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ≤ (a₁ ∪ b₁)
60	59	mlduali 1128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ a₀) ∩ (a₁ ∪ b₁)) = (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ (a₀ ∩ (a₁ ∪ b₁)))
61	58, 60	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) = (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ (a₀ ∩ (a₁ ∪ b₁)))
62		lear 161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ≤ (a₂ ∪ b₂)
63	62	leror 152	. . . . . . . . . . . . . . . . . . . . . . . . 25 (((a₁ ∪ b₁) ∩ (a₂ ∪ b₂)) ∪ (a₀ ∩ (a₁ ∪ b₁))) ≤ ((a₂ ∪ b₂) ∪ (a₀ ∩ (a₁ ∪ b₁)))
64	61, 63	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . 24 ((a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) ≤ ((a₂ ∪ b₂) ∪ (a₀ ∩ (a₁ ∪ b₁)))
65		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((a₂ ∪ b₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) = ((a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))) ∪ b₂)
66		xxdp.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 d = (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))
67	66	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (d ∪ b₂) = ((a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))) ∪ b₂)
68	67	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))) ∪ b₂) = (d ∪ b₂)
69	65, 68	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 ((a₂ ∪ b₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) = (d ∪ b₂)
70	64, 69	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . 23 ((a₀ ∪ (1 ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) ≤ (d ∪ b₂)
71	48, 70	letr 137	. . . . . . . . . . . . . . . . . . . . . 22 ((a₀ ∪ (b₀ ∩ (a₀ ∪ ((a₁ ∪ b₁) ∩ (a₂ ∪ b₂))))) ∩ (a₁ ∪ b₁)) ≤ (d ∪ b₂)
72	44, 71	bltr 138	. . . . . . . . . . . . . . . . . . . . 21 ((a₀ ∪ e) ∩ (a₁ ∪ b₁)) ≤ (d ∪ b₂)
73	37, 72	bltr 138	. . . . . . . . . . . . . . . . . . . 20 ((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ≤ (d ∪ b₂)
74	73	df2le2 136	. . . . . . . . . . . . . . . . . . 19 (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂)) = ((a₁ ∪ b₁) ∩ (a₀ ∪ e))
75	74	cm 61	. . . . . . . . . . . . . . . . . 18 ((a₁ ∪ b₁) ∩ (a₀ ∪ e)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂))
76		id 59	. . . . . . . . . . . . . . . . . . 19 (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂))
77	76	cm 61	. . . . . . . . . . . . . . . . . 18 (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂))
78	75, 77	tr 62	. . . . . . . . . . . . . . . . 17 ((a₁ ∪ b₁) ∩ (a₀ ∪ e)) = (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂))
79		id 59	. . . . . . . . . . . . . . . . . 18 ((a₀ ∪ d) ∩ (e ∪ b₂)) = ((a₀ ∪ d) ∩ (e ∪ b₂))
80		id 59	. . . . . . . . . . . . . . . . . 18 ((a₁ ∪ d) ∩ (b₁ ∪ b₂)) = ((a₁ ∪ d) ∩ (b₁ ∪ b₂))
81		orcom 73	. . . . . . . . . . . . . . . . . . 19 (a₀ ∪ a₁) = (a₁ ∪ a₀)
82		orcom 73	. . . . . . . . . . . . . . . . . . 19 (e ∪ b₁) = (b₁ ∪ e)
83	81, 82	2an 79	. . . . . . . . . . . . . . . . . 18 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = ((a₁ ∪ a₀) ∩ (b₁ ∪ e))
84	79, 80, 83, 76	dp34 1181	. . . . . . . . . . . . . . . . 17 (((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ∩ (d ∪ b₂)) ≤ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
85	78, 84	bltr 138	. . . . . . . . . . . . . . . 16 ((a₁ ∪ b₁) ∩ (a₀ ∪ e)) ≤ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
86	35, 85	lel2or 170	. . . . . . . . . . . . . . 15 ((a₁ ∪ e) ∪ ((a₁ ∪ b₁) ∩ (a₀ ∪ e))) ≤ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
87	34, 86	bltr 138	. . . . . . . . . . . . . 14 (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e)) ≤ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
88	87	lelan 167	. . . . . . . . . . . . 13 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₁ ∪ b₁) ∪ e) ∩ ((a₁ ∪ a₀) ∪ e))) ≤ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))))
89	13, 88	bltr 138	. . . . . . . . . . . 12 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ b₁) ∪ e)) ∩ ((a₁ ∪ a₀) ∪ e)) ≤ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))))
90	15, 89	bltr 138	. . . . . . . . . . 11 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))))
91		mldual 1124	. . . . . . . . . . . 12 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
92		ancom 74	. . . . . . . . . . . . 13 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁)))
93	92	lor 70	. . . . . . . . . . . 12 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁))))
94		lea 160	. . . . . . . . . . . . . 14 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ≤ ((a₀ ∪ a₁) ∩ (e ∪ b₁))
95	94	ml2i 1125	. . . . . . . . . . . . 13 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁)))) = (((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁)))
96		ancom 74	. . . . . . . . . . . . 13 (((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁))) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))
97		ax-a2 31	. . . . . . . . . . . . . 14 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)))
98	97	lan 77	. . . . . . . . . . . . 13 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e))))
99	95, 96, 98	3tr 65	. . . . . . . . . . . 12 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) ∪ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∩ ((a₀ ∪ a₁) ∩ (e ∪ b₁)))) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e))))
100	91, 93, 99	3tr 65	. . . . . . . . . . 11 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((a₁ ∪ e) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))))) = (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e))))
101	90, 100	lbtr 139	. . . . . . . . . 10 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e))))
102		mldual 1124	. . . . . . . . . . . 12 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)))
103	3	ran 78	. . . . . . . . . . . . . 14 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) = (((a₁ ∪ a₀) ∩ (b₁ ∪ e)) ∩ (a₁ ∪ e))
104		anass 76	. . . . . . . . . . . . . 14 (((a₁ ∪ a₀) ∩ (b₁ ∪ e)) ∩ (a₁ ∪ e)) = ((a₁ ∪ a₀) ∩ ((b₁ ∪ e) ∩ (a₁ ∪ e)))
105		leor 159	. . . . . . . . . . . . . . . . . 18 e ≤ (b₁ ∪ e)
106	105	mldual2i 1127	. . . . . . . . . . . . . . . . 17 ((b₁ ∪ e) ∩ (a₁ ∪ e)) = (((b₁ ∪ e) ∩ a₁) ∪ e)
107		orcom 73	. . . . . . . . . . . . . . . . 17 (((b₁ ∪ e) ∩ a₁) ∪ e) = (e ∪ ((b₁ ∪ e) ∩ a₁))
108		ancom 74	. . . . . . . . . . . . . . . . . 18 ((b₁ ∪ e) ∩ a₁) = (a₁ ∩ (b₁ ∪ e))
109	108	lor 70	. . . . . . . . . . . . . . . . 17 (e ∪ ((b₁ ∪ e) ∩ a₁)) = (e ∪ (a₁ ∩ (b₁ ∪ e)))
110	106, 107, 109	3tr 65	. . . . . . . . . . . . . . . 16 ((b₁ ∪ e) ∩ (a₁ ∪ e)) = (e ∪ (a₁ ∩ (b₁ ∪ e)))
111	110	lan 77	. . . . . . . . . . . . . . 15 ((a₁ ∪ a₀) ∩ ((b₁ ∪ e) ∩ (a₁ ∪ e))) = ((a₁ ∪ a₀) ∩ (e ∪ (a₁ ∩ (b₁ ∪ e))))
112		leao1 162	. . . . . . . . . . . . . . . 16 (a₁ ∩ (b₁ ∪ e)) ≤ (a₁ ∪ a₀)
113	112	mldual2i 1127	. . . . . . . . . . . . . . 15 ((a₁ ∪ a₀) ∩ (e ∪ (a₁ ∩ (b₁ ∪ e)))) = (((a₁ ∪ a₀) ∩ e) ∪ (a₁ ∩ (b₁ ∪ e)))
114		orcom 73	. . . . . . . . . . . . . . . 16 (((a₁ ∪ a₀) ∩ e) ∪ (a₁ ∩ (b₁ ∪ e))) = ((a₁ ∩ (b₁ ∪ e)) ∪ ((a₁ ∪ a₀) ∩ e))
115		ancom 74	. . . . . . . . . . . . . . . . 17 ((a₁ ∪ a₀) ∩ e) = (e ∩ (a₁ ∪ a₀))
116	115	lor 70	. . . . . . . . . . . . . . . 16 ((a₁ ∩ (b₁ ∪ e)) ∪ ((a₁ ∪ a₀) ∩ e)) = ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))
117	114, 116	tr 62	. . . . . . . . . . . . . . 15 (((a₁ ∪ a₀) ∩ e) ∪ (a₁ ∩ (b₁ ∪ e))) = ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))
118	111, 113, 117	3tr 65	. . . . . . . . . . . . . 14 ((a₁ ∪ a₀) ∩ ((b₁ ∪ e) ∩ (a₁ ∪ e))) = ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))
119	103, 104, 118	3tr 65	. . . . . . . . . . . . 13 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)) = ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))
120	119	lor 70	. . . . . . . . . . . 12 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))))
121	102, 120	tr 62	. . . . . . . . . . 11 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)))) = ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))))
122		lear 161	. . . . . . . . . . . 12 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ≤ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
123	122	leror 152	. . . . . . . . . . 11 ((((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))) ≤ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))))
124	121, 123	bltr 138	. . . . . . . . . 10 (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ (((a₀ ∪ a₁) ∩ (e ∪ b₁)) ∩ (a₁ ∪ e)))) ≤ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))))
125	101, 124	letr 137	. . . . . . . . 9 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))))
126		orcom 73	. . . . . . . . . . . 12 ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀))) = ((e ∩ (a₁ ∪ a₀)) ∪ (a₁ ∩ (b₁ ∪ e)))
127	126	lor 70	. . . . . . . . . . 11 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((e ∩ (a₁ ∪ a₀)) ∪ (a₁ ∩ (b₁ ∪ e))))
128		or4 84	. . . . . . . . . . . 12 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((e ∩ (a₁ ∪ a₀)) ∪ (a₁ ∩ (b₁ ∪ e)))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (e ∩ (a₁ ∪ a₀))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e))))
129		ancom 74	. . . . . . . . . . . . . . 15 ((a₀ ∪ d) ∩ (e ∪ b₂)) = ((e ∪ b₂) ∩ (a₀ ∪ d))
130	79, 129	tr 62	. . . . . . . . . . . . . 14 ((a₀ ∪ d) ∩ (e ∪ b₂)) = ((e ∪ b₂) ∩ (a₀ ∪ d))
131	130	ror 71	. . . . . . . . . . . . 13 (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (e ∩ (a₁ ∪ a₀))) = (((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (e ∩ (a₁ ∪ a₀)))
132	80	ror 71	. . . . . . . . . . . . 13 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e)))
133	131, 132	2or 72	. . . . . . . . . . . 12 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (e ∩ (a₁ ∪ a₀))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e)))) = ((((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (e ∩ (a₁ ∪ a₀))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e))))
134	128, 133	tr 62	. . . . . . . . . . 11 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((e ∩ (a₁ ∪ a₀)) ∪ (a₁ ∩ (b₁ ∪ e)))) = ((((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (e ∩ (a₁ ∪ a₀))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e))))
135		leao1 162	. . . . . . . . . . . . 13 (e ∩ (a₁ ∪ a₀)) ≤ (e ∪ b₂)
136	135	mli 1126	. . . . . . . . . . . 12 (((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (e ∩ (a₁ ∪ a₀))) = ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀))))
137		leao1 162	. . . . . . . . . . . . 13 (a₁ ∩ (b₁ ∪ e)) ≤ (a₁ ∪ d)
138	137	mli 1126	. . . . . . . . . . . 12 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e))) = ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e))))
139	136, 138	2or 72	. . . . . . . . . . 11 ((((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (e ∩ (a₁ ∪ a₀))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (a₁ ∩ (b₁ ∪ e)))) = (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e)))))
140	127, 134, 139	3tr 65	. . . . . . . . . 10 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))) = (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e)))))
141		or32 82	. . . . . . . . . . . . 13 ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀))) = ((a₀ ∪ (e ∩ (a₁ ∪ a₀))) ∪ d)
142		ml3 1130	. . . . . . . . . . . . . . 15 (a₀ ∪ (e ∩ (a₁ ∪ a₀))) = (a₀ ∪ (a₁ ∩ (e ∪ a₀)))
143		orcom 73	. . . . . . . . . . . . . . . . 17 (e ∪ a₀) = (a₀ ∪ e)
144	143	lan 77	. . . . . . . . . . . . . . . 16 (a₁ ∩ (e ∪ a₀)) = (a₁ ∩ (a₀ ∪ e))
145	144	lor 70	. . . . . . . . . . . . . . 15 (a₀ ∪ (a₁ ∩ (e ∪ a₀))) = (a₀ ∪ (a₁ ∩ (a₀ ∪ e)))
146	142, 145	tr 62	. . . . . . . . . . . . . 14 (a₀ ∪ (e ∩ (a₁ ∪ a₀))) = (a₀ ∪ (a₁ ∩ (a₀ ∪ e)))
147	146	ror 71	. . . . . . . . . . . . 13 ((a₀ ∪ (e ∩ (a₁ ∪ a₀))) ∪ d) = ((a₀ ∪ (a₁ ∩ (a₀ ∪ e))) ∪ d)
148		or32 82	. . . . . . . . . . . . 13 ((a₀ ∪ (a₁ ∩ (a₀ ∪ e))) ∪ d) = ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))
149	141, 147, 148	3tr 65	. . . . . . . . . . . 12 ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀))) = ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))
150	149	lan 77	. . . . . . . . . . 11 ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀)))) = ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e))))
151		or32 82	. . . . . . . . . . . . 13 ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e))) = ((b₁ ∪ (a₁ ∩ (b₁ ∪ e))) ∪ b₂)
152		orcom 73	. . . . . . . . . . . . . . . . 17 (b₁ ∪ e) = (e ∪ b₁)
153	152	lan 77	. . . . . . . . . . . . . . . 16 (a₁ ∩ (b₁ ∪ e)) = (a₁ ∩ (e ∪ b₁))
154	153	lor 70	. . . . . . . . . . . . . . 15 (b₁ ∪ (a₁ ∩ (b₁ ∪ e))) = (b₁ ∪ (a₁ ∩ (e ∪ b₁)))
155		ml3 1130	. . . . . . . . . . . . . . 15 (b₁ ∪ (a₁ ∩ (e ∪ b₁))) = (b₁ ∪ (e ∩ (a₁ ∪ b₁)))
156	154, 155	tr 62	. . . . . . . . . . . . . 14 (b₁ ∪ (a₁ ∩ (b₁ ∪ e))) = (b₁ ∪ (e ∩ (a₁ ∪ b₁)))
157	156	ror 71	. . . . . . . . . . . . 13 ((b₁ ∪ (a₁ ∩ (b₁ ∪ e))) ∪ b₂) = ((b₁ ∪ (e ∩ (a₁ ∪ b₁))) ∪ b₂)
158		or32 82	. . . . . . . . . . . . 13 ((b₁ ∪ (e ∩ (a₁ ∪ b₁))) ∪ b₂) = ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))
159	151, 157, 158	3tr 65	. . . . . . . . . . . 12 ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e))) = ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))
160	159	lan 77	. . . . . . . . . . 11 ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e)))) = ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁))))
161	150, 160	2or 72	. . . . . . . . . 10 (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (e ∩ (a₁ ∪ a₀)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (a₁ ∩ (b₁ ∪ e))))) = (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))))
162	140, 161	tr 62	. . . . . . . . 9 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((a₁ ∩ (b₁ ∪ e)) ∪ (e ∩ (a₁ ∪ a₀)))) = (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))))
163	125, 162	lbtr 139	. . . . . . . 8 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))))
164		lea 160	. . . . . . . . . . . 12 (a₁ ∩ (a₀ ∪ e)) ≤ a₁
165	27	leran 153	. . . . . . . . . . . . 13 (a₁ ∩ (a₀ ∪ e)) ≤ ((a₁ ∪ b₁) ∩ (a₀ ∪ e))
166	165, 73	letr 137	. . . . . . . . . . . 12 (a₁ ∩ (a₀ ∪ e)) ≤ (d ∪ b₂)
167	164, 166	ler2an 173	. . . . . . . . . . 11 (a₁ ∩ (a₀ ∪ e)) ≤ (a₁ ∩ (d ∪ b₂))
168	167	lelor 166	. . . . . . . . . 10 ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e))) ≤ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))
169	168	lelan 167	. . . . . . . . 9 ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))) ≤ ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂))))
170		lea 160	. . . . . . . . . . . 12 (e ∩ (a₁ ∪ b₁)) ≤ e
171		lear 161	. . . . . . . . . . . . . 14 (e ∩ (a₁ ∪ b₁)) ≤ (a₁ ∪ b₁)
172		leao3 164	. . . . . . . . . . . . . 14 (e ∩ (a₁ ∪ b₁)) ≤ (a₀ ∪ e)
173	171, 172	ler2an 173	. . . . . . . . . . . . 13 (e ∩ (a₁ ∪ b₁)) ≤ ((a₁ ∪ b₁) ∩ (a₀ ∪ e))
174	173, 73	letr 137	. . . . . . . . . . . 12 (e ∩ (a₁ ∪ b₁)) ≤ (d ∪ b₂)
175	170, 174	ler2an 173	. . . . . . . . . . 11 (e ∩ (a₁ ∪ b₁)) ≤ (e ∩ (d ∪ b₂))
176	175	lelor 166	. . . . . . . . . 10 ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁))) ≤ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂)))
177	176	lelan 167	. . . . . . . . 9 ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁)))) ≤ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂))))
178	169, 177	le2or 168	. . . . . . . 8 (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (a₀ ∪ e)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (a₁ ∪ b₁))))) ≤ (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂)))))
179	163, 178	letr 137	. . . . . . 7 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂)))))
180		ax-a2 31	. . . . . . . . . . . . . . 15 (d ∪ b₂) = (b₂ ∪ d)
181	180	lan 77	. . . . . . . . . . . . . 14 (a₁ ∩ (d ∪ b₂)) = (a₁ ∩ (b₂ ∪ d))
182	181	lor 70	. . . . . . . . . . . . 13 (d ∪ (a₁ ∩ (d ∪ b₂))) = (d ∪ (a₁ ∩ (b₂ ∪ d)))
183		ml3 1130	. . . . . . . . . . . . 13 (d ∪ (a₁ ∩ (b₂ ∪ d))) = (d ∪ (b₂ ∩ (a₁ ∪ d)))
184	182, 183	tr 62	. . . . . . . . . . . 12 (d ∪ (a₁ ∩ (d ∪ b₂))) = (d ∪ (b₂ ∩ (a₁ ∪ d)))
185	184	lor 70	. . . . . . . . . . 11 (a₀ ∪ (d ∪ (a₁ ∩ (d ∪ b₂)))) = (a₀ ∪ (d ∪ (b₂ ∩ (a₁ ∪ d))))
186		orass 75	. . . . . . . . . . 11 ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂))) = (a₀ ∪ (d ∪ (a₁ ∩ (d ∪ b₂))))
187		orass 75	. . . . . . . . . . 11 ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d))) = (a₀ ∪ (d ∪ (b₂ ∩ (a₁ ∪ d))))
188	185, 186, 187	3tr1 63	. . . . . . . . . 10 ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂))) = ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d)))
189	188	lan 77	. . . . . . . . 9 ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))) = ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d))))
190		ml3 1130	. . . . . . . . . . . 12 (b₂ ∪ (e ∩ (d ∪ b₂))) = (b₂ ∪ (d ∩ (e ∪ b₂)))
191	190	lor 70	. . . . . . . . . . 11 (b₁ ∪ (b₂ ∪ (e ∩ (d ∪ b₂)))) = (b₁ ∪ (b₂ ∪ (d ∩ (e ∪ b₂))))
192		orass 75	. . . . . . . . . . 11 ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂))) = (b₁ ∪ (b₂ ∪ (e ∩ (d ∪ b₂))))
193		orass 75	. . . . . . . . . . 11 ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂))) = (b₁ ∪ (b₂ ∪ (d ∩ (e ∪ b₂))))
194	191, 192, 193	3tr1 63	. . . . . . . . . 10 ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂))) = ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂)))
195	194	lan 77	. . . . . . . . 9 ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂)))) = ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂))))
196	189, 195	2or 72	. . . . . . . 8 (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂))))) = (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂)))))
197		leao3 164	. . . . . . . . . . 11 (b₂ ∩ (a₁ ∪ d)) ≤ (e ∪ b₂)
198	197	mldual2i 1127	. . . . . . . . . 10 ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d)))) = (((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (b₂ ∩ (a₁ ∪ d)))
199	130	ror 71	. . . . . . . . . . 11 (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d))) = (((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (b₂ ∩ (a₁ ∪ d)))
200	199	cm 61	. . . . . . . . . 10 (((e ∪ b₂) ∩ (a₀ ∪ d)) ∪ (b₂ ∩ (a₁ ∪ d))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d)))
201	198, 200	tr 62	. . . . . . . . 9 ((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d)))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d)))
202		leao3 164	. . . . . . . . . . 11 (d ∩ (e ∪ b₂)) ≤ (a₁ ∪ d)
203	202	mldual2i 1127	. . . . . . . . . 10 ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂)))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))
204	80	ror 71	. . . . . . . . . . 11 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))
205	204	cm 61	. . . . . . . . . 10 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))
206	203, 205	tr 62	. . . . . . . . 9 ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂)))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))
207	201, 206	2or 72	. . . . . . . 8 (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (b₂ ∩ (a₁ ∪ d)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (d ∩ (e ∪ b₂))))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂))))
208		or4 84	. . . . . . . . 9 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))) = ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂))))
209		orcom 73	. . . . . . . . 9 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) ∪ ((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂)))) = (((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂))) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))))
210		ancom 74	. . . . . . . . . . . . 13 (b₂ ∩ (a₁ ∪ d)) = ((a₁ ∪ d) ∩ b₂)
211		leor 159	. . . . . . . . . . . . . 14 b₂ ≤ (b₁ ∪ b₂)
212	211	lelan 167	. . . . . . . . . . . . 13 ((a₁ ∪ d) ∩ b₂) ≤ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))
213	210, 212	bltr 138	. . . . . . . . . . . 12 (b₂ ∩ (a₁ ∪ d)) ≤ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))
214		leor 159	. . . . . . . . . . . . 13 d ≤ (a₀ ∪ d)
215	214	leran 153	. . . . . . . . . . . 12 (d ∩ (e ∪ b₂)) ≤ ((a₀ ∪ d) ∩ (e ∪ b₂))
216	213, 215	le2or 168	. . . . . . . . . . 11 ((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂))) ≤ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂)))
217	80, 79	2or 72	. . . . . . . . . . . . 13 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂)))
218	217	cm 61	. . . . . . . . . . . 12 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂))) = (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂)))
219		orcom 73	. . . . . . . . . . . 12 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
220	218, 219	tr 62	. . . . . . . . . . 11 (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ ((a₀ ∪ d) ∩ (e ∪ b₂))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
221	216, 220	lbtr 139	. . . . . . . . . 10 ((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂))) ≤ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
222	221	df-le2 131	. . . . . . . . 9 (((b₂ ∩ (a₁ ∪ d)) ∪ (d ∩ (e ∪ b₂))) ∪ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
223	208, 209, 222	3tr 65	. . . . . . . 8 ((((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ (b₂ ∩ (a₁ ∪ d))) ∪ (((a₁ ∪ d) ∩ (b₁ ∪ b₂)) ∪ (d ∩ (e ∪ b₂)))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
224	196, 207, 223	3tr 65	. . . . . . 7 (((e ∪ b₂) ∩ ((a₀ ∪ d) ∪ (a₁ ∩ (d ∪ b₂)))) ∪ ((a₁ ∪ d) ∩ ((b₁ ∪ b₂) ∪ (e ∩ (d ∪ b₂))))) = (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
225	179, 224	lbtr 139	. . . . . 6 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) ≤ (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂)))
226	38	ror 71	. . . . . . 7 (e ∪ b₁) = ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)
227	226	lan 77	. . . . . 6 ((a₀ ∪ a₁) ∩ (e ∪ b₁)) = ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁))
228	66	lor 70	. . . . . . . 8 (a₀ ∪ d) = (a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))))
229	38	ror 71	. . . . . . . 8 (e ∪ b₂) = ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)
230	228, 229	2an 79	. . . . . . 7 ((a₀ ∪ d) ∩ (e ∪ b₂)) = ((a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂))
231	66	lor 70	. . . . . . . 8 (a₁ ∪ d) = (a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))))
232	231	ran 78	. . . . . . 7 ((a₁ ∪ d) ∩ (b₁ ∪ b₂)) = ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂))
233	230, 232	2or 72	. . . . . 6 (((a₀ ∪ d) ∩ (e ∪ b₂)) ∪ ((a₁ ∪ d) ∩ (b₁ ∪ b₂))) = (((a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂)))
234	225, 227, 233	le3tr2 141	. . . . 5 ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ (((a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂)))
235		or12 80	. . . . . . . 8 (a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) = (a₂ ∪ (a₀ ∪ (a₀ ∩ (a₁ ∪ b₁))))
236		orabs 120	. . . . . . . . 9 (a₀ ∪ (a₀ ∩ (a₁ ∪ b₁))) = a₀
237	236	lor 70	. . . . . . . 8 (a₂ ∪ (a₀ ∪ (a₀ ∩ (a₁ ∪ b₁)))) = (a₂ ∪ a₀)
238		orcom 73	. . . . . . . 8 (a₂ ∪ a₀) = (a₀ ∪ a₂)
239	235, 237, 238	3tr 65	. . . . . . 7 (a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) = (a₀ ∪ a₂)
240	239	ran 78	. . . . . 6 ((a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) = ((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂))
241		orass 75	. . . . . . . 8 ((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) = (a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁))))
242	241	ran 78	. . . . . . 7 (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂)) = ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂))
243	242	cm 61	. . . . . 6 ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂)) = (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂))
244	240, 243	2or 72	. . . . 5 (((a₀ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ ((a₁ ∪ (a₂ ∪ (a₀ ∩ (a₁ ∪ b₁)))) ∩ (b₁ ∪ b₂))) = (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂)))
245	234, 244	lbtr 139	. . . 4 ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂)))
246		ax-a2 31	. . . . . . . . . 10 (a₁ ∪ a₂) = (a₂ ∪ a₁)
247		ax-a2 31	. . . . . . . . . . 11 (a₁ ∪ b₁) = (b₁ ∪ a₁)
248	247	lan 77	. . . . . . . . . 10 (a₀ ∩ (a₁ ∪ b₁)) = (a₀ ∩ (b₁ ∪ a₁))
249	246, 248	2or 72	. . . . . . . . 9 ((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) = ((a₂ ∪ a₁) ∪ (a₀ ∩ (b₁ ∪ a₁)))
250		orass 75	. . . . . . . . 9 ((a₂ ∪ a₁) ∪ (a₀ ∩ (b₁ ∪ a₁))) = (a₂ ∪ (a₁ ∪ (a₀ ∩ (b₁ ∪ a₁))))
251	249, 250	tr 62	. . . . . . . 8 ((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) = (a₂ ∪ (a₁ ∪ (a₀ ∩ (b₁ ∪ a₁))))
252		ml3le 1129	. . . . . . . . 9 (a₁ ∪ (a₀ ∩ (b₁ ∪ a₁))) ≤ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁)))
253	252	lelor 166	. . . . . . . 8 (a₂ ∪ (a₁ ∪ (a₀ ∩ (b₁ ∪ a₁)))) ≤ (a₂ ∪ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁))))
254	251, 253	bltr 138	. . . . . . 7 ((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ≤ (a₂ ∪ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁))))
255		orass 75	. . . . . . . . 9 ((a₂ ∪ a₁) ∪ (b₁ ∩ (a₀ ∪ a₁))) = (a₂ ∪ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁))))
256	255	cm 61	. . . . . . . 8 (a₂ ∪ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁)))) = ((a₂ ∪ a₁) ∪ (b₁ ∩ (a₀ ∪ a₁)))
257		ax-a2 31	. . . . . . . . 9 (a₂ ∪ a₁) = (a₁ ∪ a₂)
258	257	ror 71	. . . . . . . 8 ((a₂ ∪ a₁) ∪ (b₁ ∩ (a₀ ∪ a₁))) = ((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁)))
259	256, 258	tr 62	. . . . . . 7 (a₂ ∪ (a₁ ∪ (b₁ ∩ (a₀ ∪ a₁)))) = ((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁)))
260	254, 259	lbtr 139	. . . . . 6 ((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ≤ ((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁)))
261	260	leran 153	. . . . 5 (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂)) ≤ (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂))
262	261	lelor 166	. . . 4 (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (a₀ ∩ (a₁ ∪ b₁))) ∩ (b₁ ∪ b₂))) ≤ (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂)))
263	245, 262	letr 137	. . 3 ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂)))
264		lea 160	. . . . . . 7 (b₀ ∩ (a₀ ∪ p₀)) ≤ b₀
265	264	leror 152	. . . . . 6 ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂) ≤ (b₀ ∪ b₂)
266	265	lelan 167	. . . . 5 ((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ≤ ((a₀ ∪ a₂) ∩ (b₀ ∪ b₂))
267		leao1 162	. . . . . . . 8 (b₁ ∩ (a₀ ∪ a₁)) ≤ (b₁ ∪ b₂)
268	267	mldual2i 1127	. . . . . . 7 ((b₁ ∪ b₂) ∩ ((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁)))) = (((b₁ ∪ b₂) ∩ (a₁ ∪ a₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))
269		ancom 74	. . . . . . 7 ((b₁ ∪ b₂) ∩ ((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁)))) = (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂))
270		ancom 74	. . . . . . . 8 ((b₁ ∪ b₂) ∩ (a₁ ∪ a₂)) = ((a₁ ∪ a₂) ∩ (b₁ ∪ b₂))
271	270	ror 71	. . . . . . 7 (((b₁ ∪ b₂) ∩ (a₁ ∪ a₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))) = (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))
272	268, 269, 271	3tr2 64	. . . . . 6 (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂)) = (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))
273	272	bile 142	. . . . 5 (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂)) ≤ (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))
274	266, 273	le2or 168	. . . 4 (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂))) ≤ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))))
275		or12 80	. . . 4 (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))) = (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))))
276	274, 275	lbtr 139	. . 3 (((a₀ ∪ a₂) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₂)) ∪ (((a₁ ∪ a₂) ∪ (b₁ ∩ (a₀ ∪ a₁))) ∩ (b₁ ∪ b₂))) ≤ (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))))
277	263, 276	letr 137	. 2 ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))))
278		xxdp.c0	. . . . 5 c₀ = ((a₁ ∪ a₂) ∩ (b₁ ∪ b₂))
279		xxdp.c1	. . . . . 6 c₁ = ((a₀ ∪ a₂) ∩ (b₀ ∪ b₂))
280	279	ror 71	. . . . 5 (c₁ ∪ (b₁ ∩ (a₀ ∪ a₁))) = (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))
281	278, 280	2or 72	. . . 4 (c₀ ∪ (c₁ ∪ (b₁ ∩ (a₀ ∪ a₁)))) = (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁))))
282	281	cm 61	. . 3 (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))) = (c₀ ∪ (c₁ ∪ (b₁ ∩ (a₀ ∪ a₁))))
283		orass 75	. . . 4 ((c₀ ∪ c₁) ∪ (b₁ ∩ (a₀ ∪ a₁))) = (c₀ ∪ (c₁ ∪ (b₁ ∩ (a₀ ∪ a₁))))
284	283	cm 61	. . 3 (c₀ ∪ (c₁ ∪ (b₁ ∩ (a₀ ∪ a₁)))) = ((c₀ ∪ c₁) ∪ (b₁ ∩ (a₀ ∪ a₁)))
285	282, 284	tr 62	. 2 (((a₁ ∪ a₂) ∩ (b₁ ∪ b₂)) ∪ (((a₀ ∪ a₂) ∩ (b₀ ∪ b₂)) ∪ (b₁ ∩ (a₀ ∪ a₁)))) = ((c₀ ∪ c₁) ∪ (b₁ ∩ (a₀ ∪ a₁)))
286	277, 285	lbtr 139	1 ((a₀ ∪ a₁) ∩ ((b₀ ∩ (a₀ ∪ p₀)) ∪ b₁)) ≤ ((c₀ ∪ c₁) ∪ (b₁ ∩ (a₀ ∪ a₁)))

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)

W3C validator