Theorem oa3moa3 1029

Description: 4-variable 3OA to 5-variable Mayet's 3OA. (Contributed by NM, 3-Apr-2009.) (Revised by NM, 31-Mar-2011.)

Hypotheses

Ref	Expression
oa3moa3.1	a ≤ b⊥
oa3moa3.2	c ≤ d⊥
oa3moa3.3	d ≤ e⊥
oa3moa3.4	e ≤ c⊥

Assertion

Ref	Expression
oa3moa3	((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))

Proof of Theorem oa3moa3

Step	Hyp	Ref	Expression
1		oa3moa3.1	. . . . . 6 a ≤ b⊥
2	1	lecon3 157	. . . . 5 b ≤ a⊥
3		oa3moa3.2	. . . . . . . 8 c ≤ d⊥
4	3	lecon3 157	. . . . . . 7 d ≤ c⊥
5		oa3moa3.4	. . . . . . 7 e ≤ c⊥
6	4, 5	lel2or 170	. . . . . 6 (d ∪ e) ≤ c⊥
7	6	lecon3 157	. . . . 5 c ≤ (d ∪ e)⊥
8	2, 7	ax-oal4 1026	. . . 4 ((b ∪ a) ∩ (c ∪ (d ∪ e))) ≤ (a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ (a ∪ (d ∪ e))))))
9		ax-a2 31	. . . . 5 (a ∪ b) = (b ∪ a)
10		ax-a3 32	. . . . 5 ((c ∪ d) ∪ e) = (c ∪ (d ∪ e))
11	9, 10	2an 79	. . . 4 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) = ((b ∪ a) ∩ (c ∪ (d ∪ e)))
12		orass 75	. . . . . . . 8 ((a ∪ d) ∪ e) = (a ∪ (d ∪ e))
13	12	lan 77	. . . . . . 7 ((b ∪ c) ∩ ((a ∪ d) ∪ e)) = ((b ∪ c) ∩ (a ∪ (d ∪ e)))
14	13	lor 70	. . . . . 6 (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))) = (c ∪ ((b ∪ c) ∩ (a ∪ (d ∪ e))))
15	14	lan 77	. . . . 5 (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) = (b ∩ (c ∪ ((b ∪ c) ∩ (a ∪ (d ∪ e)))))
16	15	lor 70	. . . 4 (a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))) = (a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ (a ∪ (d ∪ e))))))
17	8, 11, 16	le3tr1 140	. . 3 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))))
18		oa3moa3.3	. . . . . . . . . 10 d ≤ e⊥
19	18	lecon3 157	. . . . . . . . 9 e ≤ d⊥
20	3, 19	lel2or 170	. . . . . . . 8 (c ∪ e) ≤ d⊥
21	20	lecon3 157	. . . . . . 7 d ≤ (c ∪ e)⊥
22	2, 21	ax-oal4 1026	. . . . . 6 ((b ∪ a) ∩ (d ∪ (c ∪ e))) ≤ (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ (a ∪ (c ∪ e))))))
23		ax-a2 31	. . . . . . . . 9 (c ∪ d) = (d ∪ c)
24	23	ror 71	. . . . . . . 8 ((c ∪ d) ∪ e) = ((d ∪ c) ∪ e)
25		orass 75	. . . . . . . 8 ((d ∪ c) ∪ e) = (d ∪ (c ∪ e))
26	24, 25	tr 62	. . . . . . 7 ((c ∪ d) ∪ e) = (d ∪ (c ∪ e))
27	9, 26	2an 79	. . . . . 6 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) = ((b ∪ a) ∩ (d ∪ (c ∪ e)))
28		orass 75	. . . . . . . . . 10 ((a ∪ c) ∪ e) = (a ∪ (c ∪ e))
29	28	lan 77	. . . . . . . . 9 ((b ∪ d) ∩ ((a ∪ c) ∪ e)) = ((b ∪ d) ∩ (a ∪ (c ∪ e)))
30	29	lor 70	. . . . . . . 8 (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) = (d ∪ ((b ∪ d) ∩ (a ∪ (c ∪ e))))
31	30	lan 77	. . . . . . 7 (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) = (b ∩ (d ∪ ((b ∪ d) ∩ (a ∪ (c ∪ e)))))
32	31	lor 70	. . . . . 6 (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))) = (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ (a ∪ (c ∪ e))))))
33	22, 27, 32	le3tr1 140	. . . . 5 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))))
34	5	lecon3 157	. . . . . . . . 9 c ≤ e⊥
35	34, 18	lel2or 170	. . . . . . . 8 (c ∪ d) ≤ e⊥
36	35	lecon3 157	. . . . . . 7 e ≤ (c ∪ d)⊥
37	2, 36	ax-oal4 1026	. . . . . 6 ((b ∪ a) ∩ (e ∪ (c ∪ d))) ≤ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ (a ∪ (c ∪ d))))))
38		ax-a2 31	. . . . . . 7 ((c ∪ d) ∪ e) = (e ∪ (c ∪ d))
39	9, 38	2an 79	. . . . . 6 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) = ((b ∪ a) ∩ (e ∪ (c ∪ d)))
40		ax-a3 32	. . . . . . . . . 10 ((a ∪ c) ∪ d) = (a ∪ (c ∪ d))
41	40	lan 77	. . . . . . . . 9 ((b ∪ e) ∩ ((a ∪ c) ∪ d)) = ((b ∪ e) ∩ (a ∪ (c ∪ d)))
42	41	lor 70	. . . . . . . 8 (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))) = (e ∪ ((b ∪ e) ∩ (a ∪ (c ∪ d))))
43	42	lan 77	. . . . . . 7 (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))) = (b ∩ (e ∪ ((b ∪ e) ∩ (a ∪ (c ∪ d)))))
44	43	lor 70	. . . . . 6 (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) = (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ (a ∪ (c ∪ d))))))
45	37, 39, 44	le3tr1 140	. . . . 5 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
46	33, 45	ler2an 173	. . . 4 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ ((a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
47	2	lel 151	. . . . . . . . . 10 (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ≤ a⊥
48	47	lecom 180	. . . . . . . . 9 (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) C a⊥
49	48	comcom7 460	. . . . . . . 8 (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) C a
50	49	comcom 453	. . . . . . 7 a C (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))
51	2	lel 151	. . . . . . . . . 10 (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))) ≤ a⊥
52	51	lecom 180	. . . . . . . . 9 (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))) C a⊥
53	52	comcom7 460	. . . . . . . 8 (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))) C a
54	53	comcom 453	. . . . . . 7 a C (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))
55	50, 54	fh3 471	. . . . . 6 (a ∪ ((b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = ((a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
56	55	cm 61	. . . . 5 ((a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = (a ∪ ((b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
57		anandi 114	. . . . . . 7 (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) = ((b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
58	57	cm 61	. . . . . 6 ((b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) = (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
59	58	lor 70	. . . . 5 (a ∪ ((b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
60	56, 59	tr 62	. . . 4 ((a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))))) ∩ (a ∪ (b ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
61	46, 60	lbtr 139	. . 3 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
62	17, 61	ler2an 173	. 2 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ ((a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))))
63	2	lel 151	. . . . . . . 8 (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ≤ a⊥
64	63	lecom 180	. . . . . . 7 (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) C a⊥
65	64	comcom7 460	. . . . . 6 (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) C a
66	65	comcom 453	. . . . 5 a C (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))
67	2	lel 151	. . . . . . . 8 (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) ≤ a⊥
68	67	lecom 180	. . . . . . 7 (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) C a⊥
69	68	comcom7 460	. . . . . 6 (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) C a
70	69	comcom 453	. . . . 5 a C (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
71	66, 70	fh3 471	. . . 4 (a ∪ ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))) = ((a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))))
72	71	ax-r1 35	. . 3 ((a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))) = (a ∪ ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))))
73		anass 76	. . . . . 6 ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))) = (b ∩ ((c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
74	73	cm 61	. . . . 5 (b ∩ ((c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
75		anandi 114	. . . . . 6 (b ∩ ((c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
76	75	ax-r1 35	. . . . 5 ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = (b ∩ ((c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))
77		anass 76	. . . . 5 (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))) = ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
78	74, 76, 77	3tr1 63	. . . 4 ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))) = (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))
79	78	lor 70	. . 3 (a ∪ ((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))) = (a ∪ (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
80	72, 79	tr 62	. 2 ((a ∪ (b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e))))) ∩ (a ∪ (b ∩ ((d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d))))))) = (a ∪ (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))
81	62, 80	lbtr 139	1 ((a ∪ b) ∩ ((c ∪ d) ∪ e)) ≤ (a ∪ (((b ∩ (c ∪ ((b ∪ c) ∩ ((a ∪ d) ∪ e)))) ∩ (d ∪ ((b ∪ d) ∩ ((a ∪ c) ∪ e)))) ∩ (e ∪ ((b ∪ e) ∩ ((a ∪ c) ∪ d)))))

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on 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-r3 439  ax-oal4 1026

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)