Theorem test 802

Description: Part of an attempt to crack a potential Kalmbach axiom. (Contributed by NM, 29-Dec-1997.)

Assertion

Ref	Expression
test	(((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))

Proof of Theorem test

Step	Hyp	Ref	Expression
1		oran3 93	. . . . 5 (a⊥ ∪ b⊥ ) = (a ∩ b)⊥
2	1	lor 70	. . . 4 (c ∪ (a⊥ ∪ b⊥ )) = (c ∪ (a ∩ b)⊥ )
3	2	ran 78	. . 3 ((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)⊥ ) ∩ (c⊥ ∩ (c ∪ (a ∩ b))))
4	3	ax-r5 38	. 2 (((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = (((c ∪ (a ∩ b)⊥ ) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))))
5		comor1 461	. . . . . . 7 (c ∪ (a ∩ b)⊥ ) C c
6	5	comcom2 183	. . . . . 6 (c ∪ (a ∩ b)⊥ ) C c⊥
7		comor2 462	. . . . . . 7 (c ∪ (a ∩ b)⊥ ) C (a ∩ b)⊥
8	7	comcom7 460	. . . . . 6 (c ∪ (a ∩ b)⊥ ) C (a ∩ b)
9	6, 8	com2an 484	. . . . 5 (c ∪ (a ∩ b)⊥ ) C (c⊥ ∩ (a ∩ b))
10	6, 8	com2or 483	. . . . . 6 (c ∪ (a ∩ b)⊥ ) C (c⊥ ∪ (a ∩ b))
11	5, 10	com2an 484	. . . . 5 (c ∪ (a ∩ b)⊥ ) C (c ∩ (c⊥ ∪ (a ∩ b)))
12	9, 11	com2or 483	. . . 4 (c ∪ (a ∩ b)⊥ ) C ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))
13	5, 8	com2or 483	. . . . 5 (c ∪ (a ∩ b)⊥ ) C (c ∪ (a ∩ b))
14	6, 13	com2an 484	. . . 4 (c ∪ (a ∩ b)⊥ ) C (c⊥ ∩ (c ∪ (a ∩ b)))
15	12, 14	fh4r 476	. . 3 (((c ∪ (a ∩ b)⊥ ) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = (((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) ∩ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))))
16		ax-a3 32	. . . . . . 7 (((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))))
17	16	ax-r1 35	. . . . . 6 ((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = (((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))
18		ax-a2 31	. . . . . . 7 (((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c ∩ (c⊥ ∪ (a ∩ b))) ∪ ((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))))
19		anor2 89	. . . . . . . . . . 11 (c⊥ ∩ (a ∩ b)) = (c ∪ (a ∩ b)⊥ )⊥
20	19	lor 70	. . . . . . . . . 10 ((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) = ((c ∪ (a ∩ b)⊥ ) ∪ (c ∪ (a ∩ b)⊥ )⊥ )
21		df-t 41	. . . . . . . . . . 11 1 = ((c ∪ (a ∩ b)⊥ ) ∪ (c ∪ (a ∩ b)⊥ )⊥ )
22	21	ax-r1 35	. . . . . . . . . 10 ((c ∪ (a ∩ b)⊥ ) ∪ (c ∪ (a ∩ b)⊥ )⊥ ) = 1
23	20, 22	ax-r2 36	. . . . . . . . 9 ((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) = 1
24	23	lor 70	. . . . . . . 8 ((c ∩ (c⊥ ∪ (a ∩ b))) ∪ ((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b)))) = ((c ∩ (c⊥ ∪ (a ∩ b))) ∪ 1)
25		or1 104	. . . . . . . 8 ((c ∩ (c⊥ ∪ (a ∩ b))) ∪ 1) = 1
26	24, 25	ax-r2 36	. . . . . . 7 ((c ∩ (c⊥ ∪ (a ∩ b))) ∪ ((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b)))) = 1
27	18, 26	ax-r2 36	. . . . . 6 (((c ∪ (a ∩ b)⊥ ) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = 1
28	17, 27	ax-r2 36	. . . . 5 ((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = 1
29		ax-a3 32	. . . . . . 7 (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))))
30	29	ax-r1 35	. . . . . 6 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))
31		ax-a2 31	. . . . . . . . 9 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) = ((c⊥ ∩ (a ∩ b)) ∪ (c⊥ ∩ (c ∪ (a ∩ b))))
32		leor 159	. . . . . . . . . . 11 (a ∩ b) ≤ (c ∪ (a ∩ b))
33	32	lelan 167	. . . . . . . . . 10 (c⊥ ∩ (a ∩ b)) ≤ (c⊥ ∩ (c ∪ (a ∩ b)))
34	33	df-le2 131	. . . . . . . . 9 ((c⊥ ∩ (a ∩ b)) ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) = (c⊥ ∩ (c ∪ (a ∩ b)))
35	31, 34	ax-r2 36	. . . . . . . 8 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) = (c⊥ ∩ (c ∪ (a ∩ b)))
36	35	ax-r5 38	. . . . . . 7 (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))
37		coman1 185	. . . . . . . . . 10 (c⊥ ∩ (c ∪ (a ∩ b))) C c⊥
38	37	comcom7 460	. . . . . . . . 9 (c⊥ ∩ (c ∪ (a ∩ b))) C c
39		comor1 461	. . . . . . . . . . 11 (c⊥ ∪ (a ∩ b)) C c⊥
40	39	comcom7 460	. . . . . . . . . . . 12 (c⊥ ∪ (a ∩ b)) C c
41		comor2 462	. . . . . . . . . . . 12 (c⊥ ∪ (a ∩ b)) C (a ∩ b)
42	40, 41	com2or 483	. . . . . . . . . . 11 (c⊥ ∪ (a ∩ b)) C (c ∪ (a ∩ b))
43	39, 42	com2an 484	. . . . . . . . . 10 (c⊥ ∪ (a ∩ b)) C (c⊥ ∩ (c ∪ (a ∩ b)))
44	43	comcom 453	. . . . . . . . 9 (c⊥ ∩ (c ∪ (a ∩ b))) C (c⊥ ∪ (a ∩ b))
45	38, 44	fh3 471	. . . . . . . 8 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ c) ∩ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∪ (a ∩ b))))
46		ax-a2 31	. . . . . . . . . 10 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ c) = (c ∪ (c⊥ ∩ (c ∪ (a ∩ b))))
47		oml 445	. . . . . . . . . 10 (c ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) = (c ∪ (a ∩ b))
48	46, 47	ax-r2 36	. . . . . . . . 9 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ c) = (c ∪ (a ∩ b))
49		or12 80	. . . . . . . . . 10 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∪ (a ∩ b))) = (c⊥ ∪ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (a ∩ b)))
50		ax-a3 32	. . . . . . . . . . . 12 ((c⊥ ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ (a ∩ b)) = (c⊥ ∪ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (a ∩ b)))
51	50	ax-r1 35	. . . . . . . . . . 11 (c⊥ ∪ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (a ∩ b))) = ((c⊥ ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ (a ∩ b))
52		orabs 120	. . . . . . . . . . . 12 (c⊥ ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) = c⊥
53	52	ax-r5 38	. . . . . . . . . . 11 ((c⊥ ∪ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ (a ∩ b)) = (c⊥ ∪ (a ∩ b))
54	51, 53	ax-r2 36	. . . . . . . . . 10 (c⊥ ∪ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (a ∩ b))) = (c⊥ ∪ (a ∩ b))
55	49, 54	ax-r2 36	. . . . . . . . 9 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∪ (a ∩ b))) = (c⊥ ∪ (a ∩ b))
56	48, 55	2an 79	. . . . . . . 8 (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ c) ∩ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
57	45, 56	ax-r2 36	. . . . . . 7 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
58	36, 57	ax-r2 36	. . . . . 6 (((c⊥ ∩ (c ∪ (a ∩ b))) ∪ (c⊥ ∩ (a ∩ b))) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
59	30, 58	ax-r2 36	. . . . 5 ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
60	28, 59	2an 79	. . . 4 (((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) ∩ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))))) = (1 ∩ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))))
61		ancom 74	. . . . 5 (1 ∩ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))) = (((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))) ∩ 1)
62		an1 106	. . . . 5 (((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))) ∩ 1) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
63	61, 62	ax-r2 36	. . . 4 (1 ∩ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
64	60, 63	ax-r2 36	. . 3 (((c ∪ (a ∩ b)⊥ ) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) ∩ ((c⊥ ∩ (c ∪ (a ∩ b))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b)))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
65	15, 64	ax-r2 36	. 2 (((c ∪ (a ∩ b)⊥ ) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
66	4, 65	ax-r2 36	1 (((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8

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-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)