Theorem oa4to6 965

Description: Orthoarguesian law (4-variable to 6-variable proof). The first 3 hypotheses are those for 6-OA. The next 4 are variable substitutions into 4-OA. The last is the 4-OA. The proof uses OM logic only. (Contributed by NM, 19-Dec-1998.)

Hypotheses

Ref	Expression
oa4to6.oa6.1	a ≤ b⊥
oa4to6.oa6.2	c ≤ d⊥
oa4to6.oa6.3	e ≤ f⊥
oa4to6.4	g = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
oa4to6.5	h = a⊥
oa4to6.6	j = c⊥
oa4to6.7	k = e⊥
oa4to6.oa4	((h →1 g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))))) ≤ g

Assertion

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

Proof of Theorem oa4to6

Step	Hyp	Ref	Expression
1		oa4to6.oa6.1	. . . . 5 a ≤ b⊥
2	1	lecon3 157	. . . 4 b ≤ a⊥
3	2	lecon 154	. . 3 a⊥ ⊥ ≤ b⊥
4		oa4to6.oa6.2	. . . . 5 c ≤ d⊥
5	4	lecon3 157	. . . 4 d ≤ c⊥
6	5	lecon 154	. . 3 c⊥ ⊥ ≤ d⊥
7		oa4to6.oa6.3	. . . . 5 e ≤ f⊥
8	7	lecon3 157	. . . 4 f ≤ e⊥
9	8	lecon 154	. . 3 e⊥ ⊥ ≤ f⊥
10		id 59	. . 3 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )) = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
11		oa4to6.oa4	. . . 4 ((h →1 g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))))) ≤ g
12		oa4to6.5	. . . . . 6 h = a⊥
13		oa4to6.4	. . . . . 6 g = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
14	12, 13	ud1lem0ab 257	. . . . 5 (h →1 g) = (a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))
15		oa4to6.6	. . . . . . 7 j = c⊥
16	12, 15	2an 79	. . . . . . . . 9 (h ∩ j) = (a⊥ ∩ c⊥ )
17	15, 13	ud1lem0ab 257	. . . . . . . . . 10 (j →1 g) = (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))
18	14, 17	2an 79	. . . . . . . . 9 ((h →1 g) ∩ (j →1 g)) = ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))
19	16, 18	2or 72	. . . . . . . 8 ((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) = ((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))
20		oa4to6.7	. . . . . . . . . . 11 k = e⊥
21	12, 20	2an 79	. . . . . . . . . 10 (h ∩ k) = (a⊥ ∩ e⊥ )
22	20, 13	ud1lem0ab 257	. . . . . . . . . . 11 (k →1 g) = (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))
23	14, 22	2an 79	. . . . . . . . . 10 ((h →1 g) ∩ (k →1 g)) = ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))
24	21, 23	2or 72	. . . . . . . . 9 ((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) = ((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))
25	15, 20	2an 79	. . . . . . . . . 10 (j ∩ k) = (c⊥ ∩ e⊥ )
26	17, 22	2an 79	. . . . . . . . . 10 ((j →1 g) ∩ (k →1 g)) = ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))
27	25, 26	2or 72	. . . . . . . . 9 ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g))) = ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))
28	24, 27	2an 79	. . . . . . . 8 (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))) = (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))))
29	19, 28	2or 72	. . . . . . 7 (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g))))) = (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))))
30	15, 29	2an 79	. . . . . 6 (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))) = (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))))))
31	12, 30	2or 72	. . . . 5 (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g))))))) = (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))))))
32	14, 31	2an 79	. . . 4 ((h →1 g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))))) = ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))))))))
33	11, 32, 13	le3tr2 141	. . 3 ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
34	3, 6, 9, 10, 33	oa4to6dual 964	. 2 (b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))
35	34	oa6fromdual 953	1 (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ wi1 12

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

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

This theorem is used by:  oa3-2to2s  990  d6oa  997  oa6  1036